PV4 ⊧ BtorMCchecks safety properties of models with registers and memories

Application domain/field

• Model checking
• Bounded model checking

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.