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

Application domain/field

Type of tool

Model checker

Expected input

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

Format:

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.
C Model checking

Links

Repository (also contains another tool): https://github.com/hernanponcedeleon/Dat3M

Last commit date

31 March 2021

Related papers

Last publication date

23 March 2021

Related tools

Other bounded model checkers: CBMC, Nidhugg

ProVerB specific

View/edit source (Markdown)



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