PV3 ⊧ Ponochecks a user-specified property for a transition systemSMT-based model checker
- Model checking
- Symbolic model checking
- SMT-based model checking
Type of toolModel checker
- 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
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)
InternalsDesigned with three use cases in mind:
- Push-button verification
- Expert verification
- Model checker development
- Uses smt-switch
- Uses MathSAT 5 as an underlying SMT solver and interpolant producer.
- Also uses Boolector for hardware model checking problems.