Program
Verification
Book

PV3 ⊧ CIVLchecks if properties of a concurrent program have been violated

Application domain/field

Concurrent programs

Expected input

Annotated layered concurrent program

Format:

Boogie program?

Expected output

Error for any properties that are violated, including error traces.

Internals

Refinement-based verifier for concurrent programs.
Part of Boogie

Links

Code (part of Boogie): https://github.com/boogie-org/boogie
Last commit date: 02 Dec 2022 (default branch)
Last commit date: 02 Dec 2022 (last activity)

Related papers

Last publication date

14 July 2020

ProVerB specific

Markdown description: view/edit
Contained in the ProVerB22 dataset (paper + artefact)

ProVerB is a part of SLEBoK. Last updated: February 2023.