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

showthe application of our results in verification of several prominent information-flow

security and consistency in concurrent systems.

Bio.BorzooBonakdarpouris 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.