ProVerB: Program Verification Book
ProVerB is a project aimed at explaining program verification tools to practicing software developers, and at helping them to find they way around the available tools, clearly and briefly summarising the main purpose of the tool, its current status, relations to other tools, etc. You can read more about the project on the credits page or visit the dataset repository.
We classify all tools in this book as belonging to one of the six levels:
- PV0 tools manipulate given and produced software artefacts with some degree of rigour. Conceptually such artefacts then may correspond to mathematical and formal entities, but this correspondence is mostly a matter of expectations. This category should be reasonably unpopulated since we mostly avoid to include such tools listed on this website.
- PV1 tools encode the formal expectations about the artefacts that they manipulate, and report back to their users about found inconsistencies. A typical resident of this level could be a linter: a tool that analyses your program and complains about places where your program does not conform to its expectations.
- PV2 tools generate an executable artefact from a formal one that specifies the desired properties and conditions, without necessarily providing means of explicitly verifying the correctness of the synthesised code. For instance, it could be a test data generator that produces a lot of diverse test cases from a model.
- PV3 tools allow the end user to control the properties that are being checked. For instance, it could be a tool that analyses user-written assertions in the code and verifies that they are indeed always respected by the program.
- PV4 tools operate within a particular paradigm and derive their actions, conclusions and even properties that they need to check, from a built-in formal specification. For example, such a tool can guarantee freedom of deadlocks in a multi-threaded application, or data consistency in a database management system. Generated property set cannot be explicitly adjusted for tools of this level.
- 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.
- PV6 tools can handle different user-written specifications, encode a wide range of different formulae for properties, and are capable of producing proofs of such properties together with inferring the correctness of such proofs.
NB: this project is a work in progress, and thus may momentarily contain imperfect or erroneous data! Use at your own risk or get in touch!
The PV-hierarchy does not represent how “worthy” or “important” a tool is, merely how much it expects and demands of its end user, and what it can offer back. In many cases having a lower-PV-level tool is more preferable because it is easier in use and is less ambitious about the effort investment. Often tools of a lower PV-level are built “on top” of tools of higher level which they run as a backend.