Parameterized verification of open procedural programs
Aleksandar S. Dimovski · 2012
This paper describes a concrete implementation of a game-semantics based approach for verification of open program terms parameterized by a data type. The programs are restricted to be data-independent with respect to the data type treated as a parameter, which means that the only operation allowed on values of that type is equality testing. The programs can also input, output, and assign such values. This provides a method for verifying a range of safety properties of programs which contain data-independent infinite types. In order to enable verification of programs with arbitrary infinite (integer) types, the proposed method can be extended by combining it with an abstraction refinement procedure. We have developed a tool which implements this method as well as its extension, and we present its practicality by several academic examples.