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

Application domain/field

• Model checking
• Hardware model checking

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)