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

Application domain/field

• Concurrency
• Sequential consistency

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)