HomeToolsCase StudiesPublications

This website hosts software tools for quantitative verification of ANSI-C. These were developed as part of the EPSRC-funded project "Automated quantitative software verification with PRISM". There are two tools:

  • QProver, based on quantitative abstraction refinement,
  • Probity, based on program instrumentation techniques.

For details of the techniques implemented in QProver, see [KKNP09] and for information about the underlying abstraction-refinement techniques, see [KKNP10]. Further details are available in Mark Kattenbelt's PhD thesis [Kat11].

This website currently provides binary downloads and details of available case studies.

Latest News

March 2011: Mark Kattenbelt's PhD thesis, which contains details of the Probity tool, is now available.
December 2010: The QProver tool now has a website, including tool downloads and case studies.