PV4 ⊧ Dartagnanchecks assertions in a C program within a chosen memory spec
- Concurrent programs
- Weak memory models
- Model checking
Type of toolModel checker
Expected inputProgram (annotated with an assertion over the final states), and the memory model.
- 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:
- Memory model: CAT
Expected outputWhether the written assertion holds for the program under the specified memory model
InternalsDartagnan is a bounded model checker for concurrent programs under weak memory models. Uses Z3.
CommentsNote: 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