Home

Welcome to the VerCors wiki!

This wiki acts as a tutorial how to use the VerCors verifier, and (to some extent) as a guide for VerCors developers. You can find the chapters of the wiki in the Sidebar on the right. Below, we give a brief overview:

Tutorial

• Introduction describes how the VerCors verifier fits into the vast field of software verification.
  • Background is intended for people who are new to software verification (e.g. students) and explains what it is about. Advanced users can skip this.
• Installing and Running VerCors provides the practical details how to install or build VerCors and execute it afterwards (e.g. dependencies).
• Prototypal Verification Language gives an introduction to the features and syntax of VerCors' own language PVL, which is similar to Java and which is used to test and develop VerCors' capabilities. This chapter is more explanatory than the table in the Syntax Reference (see below).
• Specification Syntax describes how to annotate a program to prove its correctness. Like the previous chapter, it gives more explanations than the Syntax Reference.
• Permissions explains how to specify access permissions for heap locations, which is a crucial part of the separation logic underlying VerCors.
• Axiomatic Data Types describes several data types natively supported by VerCors (i.e. in PVL and specifications), such as sequences and sets, and the operations supported for those types.
• Arrays and Pointers explains how to specify permissions and facts when accessing heap locations indirectly, via arrays or (in C) pointers.
• Predicates describes how permissions can be grouped into predicates, which is particularly important for recursive data structures, but also helpful in other situations.
• Parallel Blocks explains a particular way to implement concurrency in PVL, and how to e.g. use permissions in that context. If you verify a program in another language (e.g. Java), this is not applicable.
• Atomics and Locks describes how VerCors natively supports critical sections and their implications on access permissions. The focus is on PVL, but it also applies to other languages (to a lesser extent).
• Process Algebra Models introduces a more advanced concept, combining the deductive verification of VerCors with model checking, in particular mCRL2 models.
• GPGPU Verification describes how to verify programs that are written in OpenCL/CUDA and to be executed on a GPU. It is a specific topic, and not relevant for users working on other systems/languages.
• Inheritance explains how VerCors supports inheritance, in particular for Java classes.
• Exceptions & Goto describes how to verify the non-linear control flow when using goto or (Java) exceptions, and what VerCors supports in that regard.
• VerCors by Error lists all the errors that VerCors can return, and potential causes for it.
• VeyMont describes the VeyMont mode allows specification, verification, and code generation for choreographies.

Advanced Concepts

Some features of VerCors are only relevant for advanced users:

• Magic Wands describes the magic wand operator -* of separation logic (a.k.a. separating implication), and how it is supported in VerCors.
• Inhale and exhale describes how to explicitly inhale and exhale permissions. Note that this can easily lead to unsoundness, and should only be used when really necessary.
• Term Rewriting Rules explains how users can add custom rules to VerCors that rewrite expressions, e.g. to simplify nested quantifiers. VerCors already has several simplification rules, so this feature is intended for advanced users working on very specific verification cases that are not well supported by VerCors.
• Profiling explains how to have VerCors output a timing profile of a verification, for measuring and diagnosing slow problems.

Annex

A few helpful resources for reference during the daily work with VerCors:

• What does this VerCors error message mean? explains some common error messages and how to fix them.
• PVL Syntax Reference provides a brief summary in tabular form of all the language constructs supported in PVL (many of which are also relevant for annotating programs in other languages). For a more detailed explanation, please refer to the chapters on PVL and the Specification Syntax (see above).
• Case Studies provides a list of case studies that have been done with VerCors.

Developing for VerCors

While this wiki is mostly directed at users of VerCors, there are also some useful resources for developers:

• VerCors Development Book (external) Former VerCors developer Pieter wrote a guide about the setup of the project and how to do certain common tasks.
• Developing for VerCors details the workflow when contributing to VerCors, e.g. reviewing of pull requests.
• Project Structure gives a brief overview of the concept behind VerCors and the directory structure of the VerCors source code.
• IDE Import explains how to set up the Vercors project in Eclipse or IntelliJ.
• Wiki Code Snippet Testing Harness is pretty meta: It explains how to write the VerCors wiki, in particular how to write code examples in a way that they are executable on the VerCors website.