Abstract
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.
César Sánchez
Research Professor
My research focuses on formal methods, in paricular logic, automata and game theory. Temporal logics for Hyperproperties. Applications to Blockchain.