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

Application domain/field

• Model checking
• Partial-order reduction

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