Software Tools

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

• CheckMate: a game-theoretic analyser of cybersecurity 

Contact: Laura Kovács.