CS Talk
Borzoo Bonakdarpour, Michigan State University
Host: Ruzica Piskac
Title: Bounded Model Checking for Hyperproperties
Abstract:
Hyperproperties are system-wide properties (rather than the property of individual execution traces). They allow dealing 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, we will discuss our recent results on bounded model checking for the temporal logics HyperLTL and A-HLTL and the accompanied tool HyperQB. We will also show the application of our results in verification of several prominent information-flow security and consistency in concurrent systems.
Bio:
Borzoo Bonakdarpour is currently an Associate Professor of Computer Science at Michigan State University. His research interests include formal methods and its application in computer security, distributed systems, and cyber-physical systems. He has published more than 120 articles and papers in top journals and conferences. His work in these areas have received multiple best paper awards from highly prestigious conferences, including, RV’21, SRDS’17, SSS’14, and SIES’10. He chaired the Technical Program Committee of the SRDS’20, SSS’16, and RV’14 conferences.