PV4 BtorMCchecks safety properties of models with registers and memories

Application domain/field

Type of tool

Model checker

Expected input


Btor2 model


BtorMC is a bounded model checker. It can check safety properties for models with registers and memories. It also produces witnesses for satisfiable properties. Uses Boolector 3.0


It is called a 'reference' bounded model checker in the paper.
Model checking


Related papers

Btor2 , BtorMC and Boolector 3.0

Last publication date

18 July 2018

Related tools

Compared to: Boolector, Yices

ProVerB specific

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