Tools

  • 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.
  • SpecLeuven (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.
    (PDF presentation)
  • 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.
  • FreeBoogie (UCD) - open source implementation of the Boogie intermediate langauge used by Spec# program verification tools developed at Microsoft research.
Comments