CS seminar: Bounded model checking for hyperproperties

Warning Icon This event is in the past.

When:
April 2, 2024
11:30 a.m. to 12:20 p.m.
Where:
Science Hall
5045 Cass Ave (Room #1125)
Detroit, MI 48202
Event category: Seminar
In-person

Speaker

Dr. Borzoo Bonakdarpour, Associate Professor, Computer Science, Michigan State University

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.

April 2024
SU M TU W TH F SA
31123456
78910111213
14151617181920
21222324252627
2829301234