PV4 BtorMCchecks safety properties of models with registers and memories

Application domain/field

Type of tool

Model checker

Expected input

Format:

Btor2 model

Internals

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

Comments

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

Links

Seems to be included in the Boolector repository: https://github.com/Boolector/boolector/tree/ad16fd1b47fdce57cc55ca5f1b2f4f7c95b2f631

Last commit date

27 May 2021

Related papers

https://doi.org/10.1007/978-3-319-96145-3_32

Last publication date

18 July 2018

Related tools

Compared to: Boolector, Yices

ProVerB specific

View/edit source (Markdown)



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