hyper
vis
Getting started
Loading...
Load Your Formula and System
Load a system and the formula that should be tested. The counter example will be generated for you.
Formula
Aiger file (*.aag):
Dot file (*.dot, optional):
Select the verification method
Bounded Model Checking
Bounded Model Checking (v2)
Bounded Model Checking (v3)
Property Directed Reachability (IC3)
Interpolation
Important:
The system must be provided as an aiger file (*.aag) and the formula must be formatted in the MCHyper input format. A dot file of the system might be generated automatically unless it is provided as an optional argument.
Load
Load Server Example
Load examples provided by the server.
Select an example
Load