MCHyper – A Model Checker for Hyperproperties
Copyright © 2020 Saarland University
Model checking has become a critical technique in the EDA industry. Since the early days of model checking, the algorithms have improved a lot and are now able to handle substantial hardware designs. Today, various complementary verification techniques are available, including binary decision diagrams (BDDs), SAT-based bounded model checking (BMC), interpolation, and Aaron Bradley’s IC3.
Temporal logics, like LTL, CTL, and CTL*, have proven to be flexible specification languages for various application areas and their verification is well understood. However, a class of system properties with ever growing importance turned our to be inherently not expressible in standard temporal logics. One example are properties that specify how information spreads (flows) in a system, so called information-flow properties. Information-flow is typically specified as the comparison of multiple executions of the system.
Recent extensions to temporal logics alleviate this shortcoming. HyperLTL and HyperCTL* introduce quantifiers that extend the quantification of CTL* by path variables. MCHyper is a model checker for the alternation-free fragments of HyperLTL and HyperCTL* that builds on the standard verification techniques from hardware model checking. Thereby, MCHyper enables the verification of hardware designs for intricate information-flow properties. HyperLTL and HyperCTL* also include properties from other application domains. The case studies that are provided with this tool include the analysis of symmetries among the processes in a mutual exclusion protocol, and the distance of code words of error resistant codes.
Availability
The source code is available on GitHub.
The initial version by Markus N. Rabe can be downloaded here: MCHyper-0.91.tar.gz Initial release including case studies, February 2015
Try MCHyper directly in your browser without installation in our online interface and learn more about the tool in the tutorial.
License
Related Publications
| [CFST19] | Verifying Hyperliveness Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. CAV 2019. Implementation |
| [DBBFH17] | Is your Software on Dope? Pedro R. D’Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns. ESOP 2017. |
| [FRS15] | Algorithms for Model Checking HyperLTL and HyperCTL* Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. CAV 2015. Implementation |
| [FR14] | The Linear-Hyper-Branching Spectrum of Temporal Logics Bernd Finkbeiner and Markus N. Rabe Information Technology 2014 |
| [CFKMRS14] | Temporal Logics for Hyperproperties Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez POST 2014 Implementation Full version available at arxiv |
| [DFKRS12] | Model Checking Information Flow in Reactive Systems Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe, and Helmut Seidl VMCAI 2012 Won the RS3 Best Paper Award! (Best among 27 papers of the RS3 project.) |
Hyper
Contact
If you have questions or problems, please contact Norine Coenen.