PV5 tools in ProVerBPV5

PV5 tools allow the end user to write their own specifications and “compile” them together with desired properties to fully formal mathematical representations that can be combined with mathematical representations of programs themselves or their desired properties, and verified together. Such a tool can already help someone make claims and guarantees about correctness, complexity or predicted performance of a novel, previously non-existing, garbage collection algorithm.

• ABC (versatile verification and synthesis arsenal)
• Attestor (checks if a property holds for a program, generates additional properties, provides examples and analysis logs)
• GenMC (given a C program with assertions and a memory model spec, reports safety errors)
• Gillian (verifies properties of a user-specified memory model)
• HolBA (library for semi-automatic analysis of binary code)
• Maude (a language and system supporting equational and rewriting logic)
• Nidhugg (given a program and a memory model, reports assertion violations)
• opaal (a lightweight variant of UPPAAL intended for rapid prototyping)
• Software Analysis Workbench (extracts an algorithmic spec from source code and uses it on backend verifiers)
• SPIN (analyses models of multi-threaded applications with different message passing paradigms or shared memory communication)
• UPPAAL (an IDE for modelling, validating and verifying networks of timed automata)
• Valgrind (framework for building dynamic analysis tools)
• xSAP (safety assessment tool for synchronous finite-state and infinite-state systems)

13 items on this list.