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

• Model checking
• Multi-threaded
• High-performance software

Type of tool

Model checker

Expected input

• LLVM IR of a program (with assertions)
• Use single or multicore (with a single queue or with work-sharing) model checker (singlecore_simple, multicore_simple, multicore_bitbetter)
• How to store states (dtree, treedbsmod, treedbs_cchm, cchm or stdmap)
• Number of threads to use

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