PV5 Nidhugggiven a program and a memory model, reports assertion violations

Stateless model checker (SMC) for C/C++ programs

Application domain/field

Type of tool

Model checker

Expected input


Expected output

It will indicate an error or state that no errors were found. The errors can be either assertion violations or robustness violations (e.g. segmentation faults).



License: GPL v3.0
C Concurrency C++ Model checking


Repository: https://github.com/nidhugg/nidhugg

Related papers

Last publication date

15 July 2021

Related tools

Other stateless model checkers: GenMC, RCMC, CDSChecker

ProVerB specific

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