Projects

This page describes current and past research projects carried out with the Vampire theorem prover. This list is not exhaustive and some projects may now be redundant.

• Interpolation
• Vinter
• Lingva, and its evolution Invgen, for invariant generation.
• Tree Interpolation
• Voogie — a verification conditions generator for simple Boogie programs. Voogie produces formulas in the FOOL logic supported by Vampire.
• Vampire higher-order - Vampire is currently in the process of being updated to support higher-order reasoning. A selection of papers on the theoretical and practical aspects of the project can be found in the publications section