Aleksandar Dimovski Compositional Software Verification Based on Game Semantics
This thesis presents a semantic framework for verifying safety proper- ties of open sequential programs. The presentation is focused on an Algol-like programming language that embodies many of the core ingredients of impera- tive and functional languages and incorporates data abstraction in its syntax. Game semantics is used to obtain a compositional, incremental way of gener- ating accurate models of programs. Model-checking is made possible by giving certain kinds of concrete automata-theoretic representations of the model. A data-abstraction re¯nement procedure is developed for model-checking safety properties of programs with in¯nite integer types. The procedure starts by model-checking the most abstract version of the program. If no counterexam- ple, or a genuine one, is found, the procedure terminates. Otherwise, it uses a spurious counterexample to re¯ne the abstraction for the next iteration. Abstraction re¯nement, assume-guarantee reasoning and the L¤ algorithm for learning regular languages are combined to yield a procedure for compositional veri¯cation. Construction of a global model is avoided using assume-guarantee reasoning and the L¤ algorithm, by learning assumptions for arbitrary subpro- grams. An implementation based on the FDR model checker for the CSP process algebra demonstrates practicality of the methods.