Tutorial
Welcome to the VerCors tutorial! In this tutorial, we will look at what VerCors is, what it can do, and how you can use it.
VerCors is a toolset for software verification. It can be used to reason about programs written in Java, C, OpenCL and PVL, which is a Prototypal Verification Language that is developed alongside VerCors and often used to demonstrate and test the capabilities of VerCors.
In this tutorial, we will first take a brief look at where VerCors fits into the bigger picture of software verification. As this is only a brief look, we recommend users that are unfamiliar with software verification to take a look at the chapter "Background" that gives more information on software verification and some of the terms used below. Then, we will discuss the syntax of PVL and Specifications in VerCors. Once we have a basic idea of how things work, we look at several more advanced concepts, either of VerCors (e.g. resources) or of the input languages (e.g. inheritance). You can find an overview of the chapters on the right.
VerCors is a verification tool that uses static analysis to prove partial correctness of a given piece of code. It requires users (e.g. software developers) to add annotations in the code, which specify the expected behaviour. The chapter "Specification Syntax" of this tutorial describes the syntax for these annotations. VerCors particularly targets parallel and concurrent programs, using the permission-based Concurrent Separation Logic (CSL) as its logical foundation. CSL is a program logic that has a very strong notion of ownership in the form of (fractional) permissions: A thread can only read from, or write to, shared memory if it owns enough permission to do so. An advantage of concurrent separation logic is that, due to the explicit handling of ownership, we get properties like data-race freedom and memory safety for free; these properties are consequences of the soundness argument of the logic. A disadvange is that it causes significant overhead to always deal with permissions explicitly. Therefore, if you only wish to verify sequential algorithms, it may be worthwhile to look at alternative tools such as OpenJML and KeY, which do not use CSL as their logical foundation. For more info on CSL, ownership and permissions, see the chapter "Permissions".
VerCors' analysis is modular, proving each method in isolation: Each method has a contract specifying the pre-conditions that must be met before calling the method, and the post-conditions that are certain when the method call finishes. Analysis of a method body happens solely based on the contract, not considering any actual calling environments.
While VerCors currently supports Java, C (incl. OpenMP), OpenCL and PVL, it is designed to be extensible, in the sense that support for other input languages with parallel and concurrent language constructs (for example C#) can be added without much difficulty. For that, the aim for VerCors is to allow reasoning over many different general concurrency structures, like statically-scoped concurrency (e.g. GPU kernels), dynamically-scoped concurrency (e.g. fork/join parallelism), and automated parallelism (e.g. programs that are automatically parallelised using OpenMP).
Note that VerCors checks for partial correctness, meaning that if the program terminates, then it satisfies its post-conditions. No proof is attempted to check whether the program actually terminates.
It is worth noting that VerCors is not the only tool that can perform static verification on annotated programs; there are actually many tools that can do a very similar job. Examples of such tools are: Dafny, OpenJML, KeY, VeriFast, and VCC. However, VerCors distinguishes itself by focussing on different parallel and concurrent language constructs (e.g. Dafny, OpenJML, and KeY only allow verifying sequential programs) of various high-level programming languages (e.g. VCC only allows to verify C programs). Moreover, VerCors is not designed to be language-dependent, and instead focusses on verification techniques for general concurrency patterns.
Internally, VerCors uses the Viper backend, which in turn uses the SMT solver Z3.
