SYRF Project

Task 3.2: "Use of the Stålmarck Method"

Abstract of deliverable 3.2.1

Back to the SYRF Home Page



The background:

Efficient theorem prover technology is essential for validation and verification. The propositional part of the Stålmarck method was invented and patented by Stålmarck, and has further been extended to include propagation rules for integer constraints. The method is based on refutation trees similar to Mondadori's proof trees, extended with a more efficient set of propagation rules, a restricted use of lemmas and a weak extension of the subformula principle. However, the efficiency of the method is essentially due to the so called saturation procedure, an exhaustive search procedure for shallow proof trees. Stålmarck defines a notion of proof depth, corresponding to the maximum number of simultaneously free assumptions in a proof. The saturation procedure then exhaustively searches for proofs up to a given depth n. The saturation procedure for a given n is polynomially time bounded in the length of the input formulas.

The saturation procedure has an obvious advantage over well-known proof techniques in applications with very large formulas and where shallow proofs can be expected. Shallow proofs can often be expected in verification and validation applications as opposed to, for instance, in combinatorial optimization.

Approach:

On the methodology side, we aim for: On the verification technique side, we aim for: Achieved Results:

An automatic interface for synchronous LSA has been developed (LSA is the language used in the ASA tool by Verilog), and a Lustre interface has been developed by Verimag.

Stronger propagation rules for arithmetical constraints have been implemented.

A hierarchical verification approach for a certain class of formulas from recursively defined synchronous arithmetical circuits has been developed. The approach includes a relaxation of the subformula principle, and, for a certain class of formulas, the hardness degree is reduced to a constant instead of growing linearly with size.

A hybrid of a constraint solver and Stålmarck's method has been implemented.

Publications:

  1. B. Carlson, M. Carlsson, and G. Stalmark.
    NP(FD): A proof system for finite domain formulas.
    Internal report. Annex A.3.2.1a