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

Format:

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.

Internals

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

Links

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

Last commit date

18 March 2018

Related papers

https://doi.org/10.1007/978-3-319-96142-2_22

Last publication date

18 July 2018

Related tools

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

ProVerB specific

View/edit source (Markdown)



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