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.


Expected output

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


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


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


Related papers

Last publication date

23 March 2021

Related tools

Other bounded model checkers: CBMC, Nidhugg

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.