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:
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].