AutoHyper – Model Checking of Hyperproperties
AutoHyper is a suit of model checkers that can check hyperproperties in finite-state systems.
It currently supports HyperLTL (AutoHyper) and HyperQPTL (AutoHyperQ).
We recommend to use AutoHyperQ which supports the more expressive logic.
AutoHyper consist of the AutoHyper and AutoHyperQ tool:
- AutoHyper: AutoHyper is a model checker for HyperLTL.
For details see:
Raven Beutner and Bernd Finkbeiner.
AutoHyper: Explicit-State Model Checking for HyperLTL.
International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023).
doi.org/10.1007/978-3-031-30823-9_8
AutoHyper can be found at github.com/AutoHyper/AutoHyper.
- AutoHyperQ: AutoHyperQ is an extension of AutoHyper that can check the more expressive HyperQPTL.
For details see:
Raven Beutner and Bernd Finkbeiner.
Model Checking Omega-Regular Hyperproperties with AutoHyperQ.
International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2023).
doi.org/10.29007/1xjt
AutoHyperQ can be found at github.com/AutoHyper/AutoHyperQ.