PV3 LLMC: Low-Level Model Checkerchecks assertions in a multi-threaded program

Multi-core explicit-state model checker of multi-threaded LLVM IR.

Application domain/field

Type of tool

Model checker

Expected input


LLVM IR file, the rest are parameters when calling the tool via the command line.


Uses DMC (model checker)


License: GNU General Public License 3.0
Concurrency LLVM Model checking


Repository: https://github.com/bergfi/llmc

Related papers

LLMC: Verifying High-Performance Software (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to: DIVINE, Nidhugg

ProVerB specific

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