PV3 Ponochecks a user-specified property for a transition system

SMT-based model checker

Application domain/field

Type of tool

Model checker

Expected input


One of the following 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)


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.


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


Repository: https://github.com/upscale-project/pono

Related papers

Pono: A Flexible and Extensible SMT-Based Model Checker (CAV '21)

Last publication date

15 July 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.