Bedwyr:
Proof certificates for model checking

This page provides examples illustrating the framework presented in the paper A framework for proof certificates in model checking [pdf] by Dale Miller and Quentin Heath. Each example demonstrates the use of one FPC (foundational proof certificate).

The definition files (usually *.def or *.thm) can be run with the Bedwyr system, for example with the command bedwyr -t -I <NAME>/harness.thm.

The files presented on this page are available as an archive (tbz, zip).

Harness

A testing harness is modelled after generic/harness.thm. It loads As there are no separate signature files, the order is important: the FPC must be loaded before the kernel, but after the logic and the certificates.
generic/harness.thm [thm]
For simplicity reasons, the logic defined in logic.thm only uses abstraction on one type, i, and Bedwyr's polymorphism is unused; these details may change in future versions of the framework. cert-sig.thm defines common certificate constructors may be used by any FPC.
logic.thm [thm]
cert-sig.thm [thm]
The file generic/fpc.thm contains a basic example of FPC, i.e. defined predicates for each clerks and experts, which use the common certificates constructors from cert-sig.thm. It is only a starting point for writing new FPCs. The FPCs from the provided examples are mostly identical to this generic FPC; the differences are marked by % XXX comments in the source files.
generic/fpc.thm [thm]
The kernel is a direct implementation of the inference rules. Thanks to the simple settings chosen ("switchable formulas"), the treatment of object-level implication can be done without Bedwyr's meta-level implication. The latter is only used in the case of unification.
kernel.thm [thm]

Examples from the paper

Reachability []

reachable/fpc.thm [thm]
adj.thm [thm]
reachable/examples.thm [thm]
reachable/harness.thm [thm]

Non-reachability []

unreachable/fpc.thm [thm]
unreachable/examples.thm [thm]
unreachable/harness.thm [thm]

Simulation []

sim/fpc.thm [thm]
lts.thm [thm]
sim/examples.thm [thm]
sim/harness.thm [thm]

Non-(bi)simulation []

nonsim/fpc.thm [thm]
nonsim/examples.thm [thm]
nonsim/harness.thm [thm]

Last modified: July 2015.