SYRF Project
Task 3.2: "Use of the Stålmarck Method"
Abstract of deliverable 3.2.2
Back to the SYRF Home Page
 

Achieved Results:

Lucifer: A tool for verifying Lustre programs
A tool that translates a Lustre program into a model in propositional logic has been developed. The model can be used for performing induction proofs in NP-Tools (which implements Stålmarck's method), where the length of the induction base (the number of times the transition function is unrolled) is given as a parameter to the translation. The verification method used is based on synchronous observers and so should be compatible with other verification efforts in SYRF. Countermodels are provided when a program fails to satisfy the required property. Because the translation is into a hierarchical network of components, matching the structure of the Lustre source, these countermodels can easily be used to trace bugs. The graphical interface of NP-Tools is useful here. Earlier Lustre to NP-Tools translators produced a large flat formula, making fault-finding difficult.

In an exciting recent development, Ed Clarke and his group have introduced the notion of bounded model checking - in which state-space exploration is limited to a certain number of steps. The method was presented in an extra talk at the recent conference on Formal Methods for CAD. This form of model checking can be coded in propositional logic so that it reduces to boolean satisfiability. First experiments in Clarke's group indicate that Stålmarck's method works very well in this context. We have begun to incorporate bounded model checking into the Lucifer tool.

Lucifer has been used to analyse a number of case studies (for example Volvo's cruise controller example,  CRISYS example of a train system). Work on Schneider's case study has just begun. The Lucifer tool is documented in Magnus Ljung's Master's thesis, which is currently in draft form. Work on Lucifer has been partially funded by SYRF.

Reducing proof hardness in Stålmarck's method
Work has continued on the addition of extra definitions of fresh variables to system formulas in order to reduce proof hardness. The extra definitions, which we call helper variables increase the set of subformulas available to the prover and can reduce branching and so proof complexity. The approach is outlined in the workshop paper by Sheeran and Borälv listed below. This year, we have concentrated on using helper variables in doing purely propositional proofs. Last year, we verified arithmetic circuits across levels of abstraction and so made heavy use of the integer arithmetic with which Stålmarck's method has been extended. We have studied the well-known pigeon hole formulas, which in their standard form have proof hardness degree that increases with size. We have reformulated them recursively, adding many new variable definitions of recursive sub-formulas, to reduce the hardness degree to one independent of size. Now, we are working on applying the lessons learned in this abstract setting to verification of synchronous circuits and programs. We have had some success in reducing the hardness of bit-level multiplier verification but we have so far been unable to reduce the hardness degree to a constant independent of size. This remains our goal. As part of this work, we have worked on reducing the hardness of proofs of some adder circuits received from SYRF partners. The Lava system that we use to generate formulas from Lustre-like programs has been described in a paper presented to the International Conference on Functional Programming.

A tutorial on Stålmarck's method
A tutorial paper on Stålmarck's method has been written. An expanded version will be submitted for journal publication. The tutorial appears as an annex to Deliverable 0.2.2.
 

Publications:

  1. P. Bjesse, K. Claessen, M. Sheeran, S. Singh.
    Lava: Hardware Design in Haskell.
    in Proc. ACM Int. Conf. on Functional Programming, Springer LNCS, 1998.

  2. Jonas Eden.
    Reducing proof hardness in propositional logic (draft), report on Master's Thesis work carried out at Prover Technology for degree at Chalmers University of Technology, Gothenburg.

  3. Magnus Ljung.
    Formal modelling and automatic verification of Lustre programs
    using NP-Tools (draft), report on Master's Thesis work carried out at Prover Technology for degree at Royal Institute of Technology, Stockholm.

  4. Mary Sheeran and Arne Borälv.
    How to prove the correctness of recursively defined circuits using Stålmarck's method.
    in Proc. Int. Workshop on Formal Techniques for Hardware and Hardware-like Systems (associated with Mathematics of Program Construction conference), Marstrand, 1998.

  5. Mary Sheeran and Gunnar Stålmarck.
    A tutorial on Stålmarck's proof procedure for propositional logic. In Proceedings of International Conference on Formal Methods in
    Computer-Aided Design (FMCAD'98), Springer LNCS, 1998.