Up: Verification via Supercompilation
Previous: Finite state systems
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.
- to identify the classes of the verification problems, where the methods
based on supercompilation are applicable;
- to provide formal proofs of correcteness of the proposed methods
and, where applicable, provide formal proofs of completeness for an
identified classes of problems;
- 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
- to perform a feasibility study on the applicability of the above
verification methods to the specifications given in the common