PV5 ⊧ Nidhugggiven a program and a memory model, reports assertion violationsStateless model checker (SMC) for C/C++ programs
- Model checking
- Stateless model checking
- Concurrent programs
- Relaxed memory models
Type of toolModel checker
- Multithreaded C/C++ program
- Each thread should be deterministic when run in isolation.
- The concurrency should be implemented with pthreads.
- Memory model
.llfile (LLVM assembly code)
- Memory model: This is passed as an argument when calling Nidhugg. It can be one of the following:
Expected outputIt 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).
- It supports the following memory models: SC, TSO, PSO, POWER and ARM.
- Nidhugg explores the possible executions to find bugs. It does this such that it will not explore executions that are equivalent to each other.