- KeY (Koblenz/Chalmers/Karlsruhe) - Interactive/automated program verification tool based on Dynamic
Logic with a user-friendly graphical interface. Supports Java,
C, and a simple while language (for teaching purposes).
- Some of the tools currently being developed at University of Aarhus:
- VeriFast is a prototype program verifier for C programs, being developed at Katholieke Universiteit Leuven, Belgium. It takes a C program annotated with separation logic contracts for specification and ghost statements for verification, and automatically verifies it using symbolic execution with a separation logic representation of memory. It has very good expressiveness and verification speed, at the expense of high annotation overhead.
- Krakatoa (LRI/INRIA) - Program verification tool for Java, builds on top of Why.
- Caduceus (LRI/INRIA) - Cousin of Krakatoa, for C.
- ESC/Java2 (UCD and others) - Second generation extended static checker for Java.
(KU Leuven) - Program verification tool for multi-threaded C# programs.
It is an adaptation of Spec# developed at Microsoft research.
- VeriCool (KU Leuven) - Automatic program verifier for Java-like programs.
- The Jahob Verification System (EPFL) - A verification system for programs written in a subset of Java.
- KIV (U Augsburg) - An interactive/automated program verifier for Java based on Dynamic Logic.
- Nit (IRISA Rennes) - A nullness annotation inferencer for Java bytecode.
Miscellaneous other tools:
- GenUTest (Tel Aviv) - A unit test and mock aspect generation tool.
- Failboxes (KU Leuven) - Methodology to provably preserve safety properties in the presence of unchecked exceptions and errors.
- Poitin (Dublin City University) - Automatic first-order theorem proved developed by Geoff Hamilton.
- Umbra and JML2BML (Warsaw University and others) - Support for specification of Java bytecode with BML.
- Canapa (Warsaw University) - Non-nullness annotation generator for JML.
- BONc (UCD) - tool support for BON specification language.
- CVPP (U Twente, KTH) - Toolset for Compositional Verification. (PDF presentation)
Frameworks, intermediate languages and tool support:
- Why (LRI/INRIA) - intermediate language used by Caduceus and Krakatoa.
(UCD) - open source implementation of the Boogie intermediate langauge
used by Spec# program verification tools developed at Microsoft