Verification Examples and Statistics.

A detailed list of verification examples can be found here.

Dowloadable version of the toolset.

See github

List of publications.

The full list of publications related to VerCors can be found here.

Online version of the toolset.

The online version has been set up using the Puptol engine.

Running a given example.

Running one of the prepared examples is simple:
  1. Select the example from the drop down menu.
  2. Click check to run the tool.

For more information on the examples look here.

Entering your own example.

To enter a new example, you can enter it in the text widget, fill out the options and click check. To save your work for later, you can use the Permalink button. Note that in case that we need to reclaim space, we will just delete them. It is however, the perfect way to send a bug report.

The options are
  1. Language: can be set to Java or PVL (the toy Language used in the Program Verification course).
  2. Backend: the verifier back-end:
    • Boogie for sequential programs
    • Chalice for programs with resource annotations.
  3. predicate handling
    • When the predicates used are with Chalice syntax direct can be used.
    • When functions are use as predicates in a non-recursive way then inline may be used.
    • When complex predicates are used, the witness encoding must be used.
  4. To see the file as it is passed to the back end, check the show backend encoding box.
  5. When verififying a kernel under the assumption of a single work group, check the single group box.

UT_Logo_2400_Black_EN.png (60 KB) Wojciech Mostowski, 02 Dec 2013 16:28