Supercompilation and Verification: an idea

Our idea here, to use supercompilation for the purpose of verification, came from the numerous observations on the results of supercompilation. It is often the case that transformed program is much simpler than original one, and moreover, the attempts to execute a program with the parameterised entry point (partially defined input), undertaken by a supercompiler reveal deep properties of the computation of this program, otherwise hidden in the original syntax. Bearing this in mind we came up with the following idea for verification via supercompilation:

Take a program/protocol/system to be verified and encode it as a functional program with a parameterized input. Then apply supercompilation in order to get an equivalent transformed program for which the correctness condition can be easily checked.

At first glance this looks like wishful thinking. To our surprise, however, this recipe worked very well for many examples, and the correctness conditions for the transformed program could be checked just by looking for simple syntactical properties. Actually, we encode the check of the correctness conditions in a program itself, so the program

• first models the execution of a system (protocol) for n steps (where n is an input parameter); and then
• checks the correctness condition.

Many systems and protocols assume non-deterministic execution. We model non-determinism by providing another input parameter, taking strings of characters as possible values. When a program needs to model a non-deterministic step (choice out of several possible transitions) it reads the next symbol of an input string which determines a particular choice. Supercompilation works on programs with input parameters and analyses possible behaviours of the program with all possible values of input parameters. Because of that, the result of supercompilation may contain (and usually it does) an information about all possible traces of the encoded protocol. One can use then this information to check safety properties.