PV3 Avytakes a model and a property and checks satisfiability within bounds

Application domain/field

Type of tool

Model checker

Expected input

Transition system (initial state, transition relation and bad states)

Format:

AIGER format

Expected output

SAT or UNSAT

Internals

SAT-based model checker Bounded model checking (it proves that a property P holds up to bound N)
Model checking

Links

Related papers

https://doi.org/10.1007/978-3-030-25543-5_21

Last publication date

12 July 2019

Related tools

ABC

ProVerB specific

View/edit source (Markdown)



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