VerCors usage tips

If you're working on a project with VerCors, you’re welcome to join the VerCors community chat. Feel free to ask any question, big or small. The chat is an informal place to get help and lowers the barrier to getting started. Send a message to vercors@lists.utwente.nl so we can invite you!

---

General Usage

To verify a file:

vct <inputFile>

---

Commonly Used Flags

• --help – Displays all available options.

---

Backend Selection

By default, VerCors uses the Silicon backend, which is based on symbolic execution.

Alternatively, you can use the Carbon backend:

--backend carbon

Carbon generates verification conditions and passes them to Boogie.
In most cases, Silicon is the best option, but sometimes Carbon performs better.

---

Watch Mode

Enable watch mode with:

--watch

This allows VerCors to automatically verify the specified file after edits.
It greatly speeds up verification after the first run and is highly recommended.

---

Advanced Verification Flags

Detection of Unsound Preconditions

Flag:

--dev-no-sat

Turns off detection of unsound preconditions.
It is not needed for general use, but may help if you have many forall statements and verification is slow.

Java example:

class C {
    //@ requires 1 == 2; // <-- Normally this causes an error; --dev-no-sat turns this off
    void m() { }
}

---

Disable Consistency Checks

Flag:

--dev-unsafe-optimization

Turns off internal checks, which can greatly decrease running time, especially for larger files. Implies --dev-no-sat.
This does not impact the verification result; however, when errors occur, they are often less readable.

---

Non-linear Arithmetic Solver

VerCors relies on SMT solvers such as Z3 to check verification conditions.
However, non-linear arithmetic is generally undecidable.

Example PVL code that does not verify:

requires x > 0 && a > 0 && n > 0 && x < n && x < a;
void f(int x, int a, int n) {
  assert a * x + x < a * n;
}

If you are working with non-linearity, we suggest enabling Z3’s non-linear solver with the following flag:

--prover-config:smt.arith.solver=6

With this option, the above example verifies.

---

Debugging Flags

View Backend Files

VerCors translates its inputs to the Viper intermediate verification language. When verification fails and the error message does not help, it can be useful to inspect the generated backend file and verify it directly using the Viper plugin for VS Code.

To inspect the generated backend file, add the following flag:

--backend-file-base <outputFile>

This creates a file named <outputFile>-0.vpr.
Often, it is useful to also pass --dev-no-sat to avoid superfluous verification errors about preconditions.

Note

The Viper version used by VerCors and the Viper VS Code plugin might be out of sync.
The Viper VS Code plugin has a 100-second timeout (which can be disabled).

---

View Output Before/After Internal Passes

Flags:

--output-before-pass:<pass>=<path>
--output-after-pass:<pass>=<path>

Shows the internal AST before and after a pass.
Run:

vct --help-passes

to list all pass names.

---

Starter Example Files

Located in the examples folder:

• concepts/basic/BasicAssert.java
• concepts/parallel/block-par.pvl
• demo/demo1.pvl, demo/demo2.pvl

Additional examples are available in the wiki/tutorial.