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:
developing automatic translators from synchronous languages
developing a higher-level requirement language
for expressing properties on synchronous systems, and compiling it
downto a low-level language upon which verification is made.
On the verification technique side, we aim for:
merging the propagation and assumption rules of the Stålmarck
method with constraint solving techniques, therby achieving
an interesting hybrid algorithm;
adding stronger propagation rules in order to reduce the
hardness degree, and to strengthen the proof system;
relax of the subformula principle in order to reduce that hardness degree
for (some set or class of) valid (tautological) formulas;
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:
B. Carlson, M. Carlsson, and G. Stalmark.
NP(FD): A proof system for finite domain formulas.
Internal report.
Annex A.3.2.1a