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

Concurrency

Links

Code (part of Boogie): https://github.com/boogie-org/boogie

Last commit date

4 June 2021 (31 March 2021 if only looking at boogie/Source/Concurrency where CIVL is located)

Related papers

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.