Verifying annotated program families using symbolic game semantics

In this paper, we propose an efficient game semantics based approach for verification of open program families, i.e. program families with undefined components (identifiers). We use symbolic representation of algorithmic game semantics, where symbolic values for inputs are used instead of concrete ones. In this way, we can compactly represent program families with infinite integers as so-called (finite state) featured symbolic automata. Specifically designed model checking algorithms are then employed to uniformly verify safety of all programs (variants) from a family at once using a single compact model and to pinpoint those programs that are unsafe (respectively, safe). We present a prototype tool implementing this approach, and we illustrate its practicality with several examples.