PV4 Yogar-CBMCconverts a multi-threaded program into an event order graph and verifies its sequential consistency

Application domain/field

Type of tool

Monoverifier

Expected input

Multi-threaded C program

Format:

C

Expected output

Proof of safety or a feasible counterexample

Internals

Constructs and refines an EOG (Event Order Graph)
C Concurrency

Links

SV-Comp: https://gitlab.com/sosy-lab/sv-comp/archives/-/blob/master/2018/yogar-cbmc.zip

Last commit date

28 Nov 2017

Related papers

https://doi.org/10.1007/978-3-319-89963-3_25

Last publication date

14 Apr 2018

ProVerB specific

View/edit source (Markdown)



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