Compositional software verification based on game semantics and process algebra

We present an approach to software model checking based on game semantics and the CSP process algebra. Open program fragments (i.e. terms-in-context) are compositionally modelled as CSP processes which represent their game semantics. This translation is performed by a prototype compiler. Observational equivalence and regular properties are checked by traces refinement using the FDR tool. We also present theorems for parameterised verification of polymorphic terms and properties. The effectiveness of the approach is evaluated on several examples. We acknowledge support by the EPSRC (GR/S52759/01). The second author was also supported by the Intel Corporation, and is also affiliated to the Mathematical Institute, Serbian Academy of Sciences and Arts, Belgrade