Automata, Logic and Games
(22 August - 25 September 2016)

 

Organizing Committee · Visitors and Participants · Overview · Activities · Venue

 

Organizing Committee

 

Co-chairs

• Anthony Widjaja Lin (Yale-NUS College and National University of Singapore)
• Luke Ong (University of Oxford)

Members

• Rajeev Alur (University of Pennsylvania)

• MikoÅ‚aj BojaÅ„czyk (University of Warsaw)
• Jin Song Dong (National University of Singapore)
• Javier Esparza (Technische Universität München)
• Joxan Jaffar (National University of Singapore)
• Naoki Kobayashi (The University of Tokyo)
• Marta Kwiatkowska (University of Oxford)
• Anca Muscholl (Université Bordeaux)
• David S. Rosenblum (National University of Singapore)

• Moshe Y. Vardi (Rice University)
• Igor Walukiewicz (Université Bordeaux and Centre National de la Recherche Scientifique)
  
  

Visitors and Participants

 

• Overseas visitors
• Local visitors
• Graduate students
• Registered local participants

 

Overview

As computing systems become larger, more complex, and increasingly distributed and interactive, there is a pressing need for formal methods that guarantee their reliability, correctness, and efficiency. The enormous cost of validating new designs has driven the search for powerful techniques of construction, modelling and verification of computing systems. Unlike physical systems, computing systems are "discontinuous", in the sense that a minor change in the input may cause major changes in the output behaviour. Consequently, standard methods of testing that are common in engineering sciences, while still useful, cannot be sufficient. A consensus is emerging in both industry and academic that the use of appropriate mathematics backed up by computer-aided design and verification tools is no longer a luxury, but a necessity.

Logic and automata-theoretic methods have been used in the specification, design and verification of hardware and software systems for decades, starting from early work on digital circuit design. A breakthrough was achieved in the 1960s by Church, Buchi, Rabin and others who showed the expressive equivalence of automata and logical systems (monadic second-order logic over infinite words and trees, in particular). Their work is the basis of a general framework for reasoning about implementation (automata) and specification (logic), yielding algorithms for checking consistency of specifications and correctness of implementations.

The study of games is a thread that runs through logic and algorithm. We are mainly concerned with two-player games on (finite or infinite) graphs with (finite or infinite) plays. Games capture in a natural and intuitive way the interaction between an (open) system and its environment. This games perspective has led to new algorithmic directions in verification on the one hand, and given rise to innovative methods of giving semantics of computation on the other.

More generally, the triumvirate of logic, automata and games is the basis of an elegant and powerful theory for the algorithmic and semantic analysis of computing systems. The model checking technology for the automatic verification of computing systems, which is based on these foundations, has seen substantial developments in the last three decades.

The proposed programme is concerned with both the theory and practice of verification. An objective of the programme is to promote interactions between researchers working in the theory and foundations of automata, logic and games, and those who build tool implementations of model checking algorithms, perform empirical studies, and work with the verification industry.

The five-week programme will focus on the following topics:

 

• Communicating, Distributed and Parameterized Systems
• Constraint Solving
• Higher-Order Model Checking
• Probabilistic Model Checking
• Timed Systems
  
  

Activities

• Week 1: 22 - 25 August 2016, Theme: Communicating, Distributed and Parameterized Systems (CDPS)
  Organisers: Mikolaj Bojanczyk and Anca Muscholl
• INFINITY 2016 Workshop: 26 August 2016
  Organisers: Matthew Hague and Anthony Lin
  Venue: IMS Auditorium
• Week 2: 29 August - 2 September 2016, Theme: Constraints
  Organisers: Joxan Jaffar and Anthony Lin
• Week 3: 5 - 9 September 2016, Theme: Quantitative Model Checking (QMC)
  Organisers: Rajeev Alur, Jinsong Dong, Marta Kwiatkowska and David Rosenblum
• Week 4: 12 - 16 September 2016, Annual Meeting of IFIP Working Group 2.2
  Organisers: Igor Walukiewicz and Javier Esparza
• Week 5: 19 - 23 September 2016, Higher-Order Model Checking (HOMC) + Communicating, Distributed and Parameterised Systems (CDPS)
  Organisers: Naoki Kobayashi & Luke Ong (HOMC); and Javier Esparza (CDPS).
• Public Lectures

	Date:	Tuesday, 30 August 2016
	Venue:	Performance Hall, Yale-NUS College, 18 College Avenue West 138528
	6:30pm - 7:30pm	Humans, Machines, and Work: The Future is Now Moshe Y. Vardi, Rice University, USA
	Date:	Thursday, 1 September 2016
	Venue:	Lecture Theatre 31, National University of Singapore Block S16, Level 3, 6 Science Drive 2, Singapore 117546
	6:30pm - 7:30pm	The Automated-Reasoning Revolution: From Theory to Practice and Back Moshe Y. Vardi, Rice University, USA

 

Please note that our office will be closed on the following public holiday.

- 12 Sep 2016 (Hari Raya Haji)

 

Students and researchers who are interested in attending these activities are requested to complete the online registration form.

The following do not need to register:

• Those invited to participate.

 

Venue

 

• IMS Auditorium

Organizing Committee · Visitors and Participants · Overview · Activities · Venue