My group is involved in the development of the following tools:
- Vampire: an automated first-order theorem prover
- leading the development of Vampire with support for program analysis and verification
- Polar: a static loop analyzer with probabilistic reasoning
- Z3: extending Z3 with custom theory support, especially for arithmetic reasoning
- Aligator : a package for loop invariant generation.
Contact: Laura Kovács.