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

Format:

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

Internals

Uses DMC (model checker)

Comments

License: GNU General Public License 3.0
Concurrency LLVM Model checking

Links

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

Last commit date

1 June 2021

Related papers

https://doi.org/10.1007/978-3-030-81688-9_32 (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to: DIVINE, Nidhugg

ProVerB specific

View/edit source (Markdown)



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