Gastvortrag: Borzoo Bonakdarpour: Bounded Model Checking for Hyperproperties

Mittwoch, 08.12.2021, 10.30 Uhr

Ort: Online Session

Vortragender: Borzoo Bonakdarpour

 

Abstract:

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.