• Load Your Formula and System

    Load a system and the formula that should be tested. The counter example will be generated for you.
    Formula
    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 Server Example

    • Status checks for

    These are the current status results for the selected project.
    To execute them, please make a selection and choose "Execute"

    No checks available

    Welcome to HyperVis

    HyperVis is a tool for running model checking of hyperproperties and visualizing occuring counterexamples.

    Continue
    Continue where you stopped. You find your existing projects on the left.
    Start Fresh
    You can start from scratch and create a new system. You can provide it as Aiger, DFA, or DOT representation.
    Play Around
    You can use one of the available examples to experiment and understand how HyperVis works.