PV4 ⊧ Dartagnanchecks assertions in a C program within a chosen memory spec

Application domain/field

• Concurrent programs
• Weak memory models
• Model checking

Type of tool

Model checker

Expected input

Program (annotated with an assertion over the final states), and the memory model.

Format:

• Program: PPC, x86, AArch64 assembly, subset of C11, or own .pts format (all limited to the subsets supported by Herd's .litmus format)
• Assertion in program should be written with the SVCOMP command: __VERIFIER_assert
• Memory model: CAT

Expected output

Whether the written assertion holds for the program under the specified memory model

Internals

Dartagnan is a bounded model checker for concurrent programs under weak memory models. Uses Z3.

Comments

Note: repository only mentions that it supports programs written in the .litmus or .bpl (Boogie) formats. However, for .bpl files you have to specify the architecture as none, tso, power, arm or arm8.