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.