This program aims at the development of the theoretical foundations of computer systems (TFCS). This field of research was intensively developed over the last three decades, yielding major improvements in model checking techniques as well as in satisfiability solving. The major challenge in the field is the need for scalability. The program aims at bringing together leading researchers on these themes. TFCS is collocated with a closely related program on satisfiability (SAT). 

The program will focus on the following aspects:

• New developments in logic:  Logic is often used in TFCS as a specification formalism, describing in a formal and rigorous way the requirements that a system under design or under verification is expected to satisfy.
• New developments in automata:  Automata are used in TFCS both as a modeling formalism, for example, transducers are used to model reactive systems, and as reasoning tools, as in the automata-theoretic approach to temporal model checking.
• Probabilistic modeling in the analysis of systems:  Probabilistic methods are used in the modeling and analysis of systems that exhibit probabilistic behavior, from randomized algorithms to biological systems.
• The use of games and their equilibria:  Games are used in TFCS both as an algorithmic construct, for example, in the usage of alternating automata in temporal model checking, and as a modeling construct, for example, in the design of reactive systems it is convenient to consider the setting as a game between the system and its environment. Once multi-agent systems are considered, equilibria enter in a natural way.
• Techniques for the analysis of cyber-physical systems:  Many features of real systems, for example time and energy usage, are quantitative, and to express these one needs continuous, real-valued functions and suitable hybrid combinations of discrete and quantitative constructs.