A proof theory for model checking

  (Dale Miller)


Model checking was introduced in the early 1980's as a way to
establish properties about (concurrent) computer programs that were
hard or impossible to establish using the traditional axiomatic proof
techniques of Floyd and Hoare. In this talk, I will show that the
proof theory of the sequent calculus---introduced by Gentzen in the
1930's, sharpened by Girard in the late 1980's, and further extended
with a treatment of fixed points---can provide an appealing foundation
of model checking based on proof.

Since the emphasis of model checking is on establishing the truth of a
property in a model, the proof theoretic notion of additive inference
rule is central: such rules allow provability to directly describe
truth conditions. Unfortunately, the additive treatment of quantifiers
requires inference rules to have infinite sets of premises and the
additive treatment of model specifications (usually given as Horn
clauses) provides no natural notion of state exploration. On the other
hand, the multiplicative treatment of quantification yields finitary
rules for them and the multiplicative treatment of Horn clauses yields
reachability algorithms.

By employing a focused proof system, it is possible to construct large
scale, synthetic rules that qualify as additive but which are built up
from multiplicative inference rules. These additive synthetic
rules---essentially rules built from the description of a
model---allow state exploration to be naturally modeled.

This is joint work with Quentin Heath.