PV3 ⊧ Ponochecks a user-specified property for a transition system

SMT-based model checker

Application domain/field

• Model checking
• Symbolic model checking
• SMT-based model checking

Type of tool

Model checker

Expected input

• Transition system
• Property to check

Format:

One of the following

• Manually built transition system (can use the API to do this)
• BTOR2 format
• (subset of) nuXmv's SMT-based theory extension of SMV
• CoreIR

The authors note that you could also use Verilog, by first using a tool to translate from Verilog to BTOR2 or SMV. The property is represented as an smt-switch formula.

Expected output

UNKNOWN if the result could not be determined, FALSE if the property does not hold, TRUE if the property holds, or ERROR in case of an internal error. When the property does not hold, then Pono will give a witness trace (either in BTOR2 witness format or the VCD standard format)

Internals

Designed with three use cases in mind:

1. Push-button verification
2. Expert verification
3. Model checker development

The user can ask the tool to attempt to prove the property with or without a bound. If the proof attempt failed then the user can ask for a counterexample trace.If the proof attempt succeeded then Pono can return an inductive invariant that implies the property.

• Uses smt-switch
• Uses MathSAT 5 as an underlying SMT solver and interpolant producer.
• Also uses Boolector for hardware model checking problems.

Comments

Pono was developed as the next generation of CoSA and was originally named cosa2.