Guest Talk: Borzoo Bonakdarpour: Bounded Model Checking for Hyperproperties
Wednesday, December 08, 2021, 10:30am
Location: Online Session
Speaker: 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.