Alexei Lisitsa (University of Liverpool), Uniform testing + supercompilation = verification

We present an approach to the verification of parameterised systems which is based on program transformation technique known as supercompilation. In that approach verification is achieved by a kind of uniform parameterised testing.

We translate the statements about safety properties of a parameterised system to be verified into the statements about the properties of the program that simulates and tests the system. The supercompilation is used then to establish the required properties of the program, typical example of which is that the program never returns the value False (no negative test results). The entry point of the program describes the constraints on the initial states of the system. During the generalisation phase of supercompilation process new entry points (input constraints) for the resulting program are constructed. Because of that, in some cases, one can establish correctness of the system (protocol) under more general constraints on the initial state than it is formulated in the original specification.

Supercompiler SCP4 for the functional programming language Refal is used for experiments.

This is a joint work with Andrei Nemytykh, Program Systems Institute of RAS, Pereslavl-Zalessky, Russia.