PV3 DPU: Dynamic Program Unfolderdetects violations of user-defined and assumed assertions

Application domain/field

Type of tool

Model checker

Expected input

A POSIX multi-threaded program


C program that is data-deterministic

Expected output

Whether it has detected any assertion violations, abort calls, exit calls with a non-zero exit code, data races or deadlocks.


Stateless model checker for C programs with POSIX threading
C Concurrency Model checking


Repository: https://github.com/cesaro/dpu

Related papers

Quasi-Optimal Partial Order Reduction

Last publication date

18 July 2018

Related tools

Mentioned in the README of the repository: POET, Nidhugg, CHESS, and Maple

ProVerB specific

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