MCHyper

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.

Checkout the Source

Publications

• Verifying Hyperliveness
  Norine Coenen, Bernd Finkbeiner, Cesar Sanchez and Leander Tentrup · CAV 2019
• Is your software on dope? ⋆ Formal analysis of surreptitiously “enhanced” programs
  Pedro R. D’Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner and Holger Hermanns · ESOP 2017
• Algorithms for Model Checking HyperLTL and HyperCTL*
  Bernd Finkbeiner, Markus N. Rabe and César Sánchez · CAV 2015
• The Linear-Hyper-Branching Spectrum of Temporal Logics
  Bernd Finkbeiner and Markus N. Rabe · it
• Temporal Logics for Hyperproperties
  Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe and César Sánchez · POST14
• Model Checking Information Flow in Reactive Systems
  Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe and Helmut Seidl · VMCAI 2012 · RS3 Best Paper Award 2011/2012