ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 17:30 - 18:00 at SUN I - Monitoring and Runtime Verification Chair(s): Ondrej Lengal

Verifying hyperproperties at runtime is a challenging problem as hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. It is necessary to store previously seen traces, because every new incoming trace needs to be compatible with every system run observed so far. Furthermore, the new incoming trace poses requirements on future traces. In our monitoring approach, we focus on those requirements by rewriting a hyperproperty in the temporal logic HyperLTL to a Boolean constraint system. A hyperproperty is then violated by multiple runs of the system if the constraint system becomes unsatisfiable. We compare our implementation, that utilizes either BDDs or a SAT solver to store and evaluate constraints, to the automata-based monitoring tool RVHyper.

Thu 11 Apr

tacas-2019-papers
16:30 - 18:00: TACAS 2019 - Monitoring and Runtime Verification at SUN I
Chair(s): Ondrej LengalBrno University of Technology
tacas-2019-papers16:30 - 17:00
Talk
Link to publication
tacas-2019-papers17:00 - 17:30
Talk
Joshua DawesUniversity of Manchester and CERN, Giles RegerUniversity of Manchester, Giovanni Franzoni, Andreas Pfeiffer, Giacomo Govi
Link to publication
tacas-2019-papers17:30 - 18:00
Talk
Link to publication