Project S1 develops algorithms for the compositional verification of complex distributed systems. The algorithms analyze partial designs, in which parts of the system are abstracted as "black boxes", and derive properties of the full system from properties of the partial designs. The central goal of the project is to increase the scalability and precision of the analysis, based on algorithms and heuristics for solving infinite games, including timed games and games with incomplete information, algorithms for QBF-solving, and methods

for automatic abstraction refinement. New themes in the third funding period are the analysis of parameterized systems and the synthesis of correctness certificates.