Gastvortrag: Borzoo Bonakdarpour: Bounded Model Checking for Hyperproperties
Mittwoch, 08.12.2021, 10.30 Uhr
Ort: Online Session
Vortragender: Borzoo Bonakdarpour
Hyperproperties are system-wide properties (rather than the property of individual execution traces). They allow us to deal with important information-flow security policies (e.g., non-interference), consistency models in concurrent computing (e.g., linearizability), and robustness models in cyber-physical systems.
In this talk, I will discuss our recent results on bounded model checking for the temporal logic HyperLTL and the accompanied tool HyperQube. I will also show the application of our results in (1) synthesizing refinements that preserve hyperproperties, and (2) path planning in multi-agent robotics systems in adversarial settings.