Future Work

The experiments have revealed the power of this non-traditional application of supercompilation for verification purposes. We plan to continue development of corresponding techniques both experimentally and theoretically setting up the following research programme.

1. to identify the classes of the verification problems, where the methods based on supercompilation are applicable;
2. to provide formal proofs of correcteness of the proposed methods and, where applicable, provide formal proofs of completeness for an identified classes of problems;
3. to provide experimental and theoretical analysis of hard cases of verification falling outside the above identified classes, but still being amenable to verification by supercompilation; and
4. to perform a feasibility study on the applicability of the above verification methods to the specifications given in the common specification languages.