Vampyre
Vampyre is an
automated theorem prover based on the Nelson-Oppen architecture for cooperating
decision procedures. Vampyre generates explicit proof representations of proved
theorems in an LF-like syntax. Vampyre was written to produce explicit proofs
of verification conditions generated from programs for
Proof Carrying Code
applications. It can also be used as a general purpose automatic theorem prover.
Vampyre is written in Ocaml.
Vampyre was developed
as a class project for George
Necula’s Automated
Deduction class. Vampyre was
written by
