Sciweavers

CAV
2015
Springer

Algorithms for Model Checking HyperLTL and HyperCTL ^*

8 years 6 months ago
Algorithms for Model Checking HyperLTL and HyperCTL ^*
We present an automata-based algorithm for checking finite state systems for hyperproperties specified in HyperLTL and HyperCTL∗ . For the alternation-free fragments of HyperLTL and HyperCTL∗ the automaton construction allows us to leverage existing model checking technology. Along several case studies, we demonstrate that the approach enables the verification of real hardware designs for properties that could not be checked before. We study information flow properties of an I2C bus master, the symmetric access to a shared resource in a mutual exclusion protocol, and the functional correctness of encoders and decoders for error resistant codes.
Bernd Finkbeiner, Markus N. Rabe, César S&a
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CAV
Authors Bernd Finkbeiner, Markus N. Rabe, César Sánchez
Comments (0)