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.
- 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