HYPER 2021

Workshop on Hyperproperties: Advances in Theory and Practice

18 October 2021 @ ATVA 2021

The study of hyperproperties has recently gained a great deal of attention in the formal methods, security, and cyber-physical systems communities. The goal of HYPER 2021 is to foster the exchange of ideas on the topic of hyperproperties between researchers from these diverse communities and to present and discuss recent advances in logical formalisms for specifying hyperproperties, algorithmic methodologies for the verification, synthesis, and runtime verification of hyperproperties, as well as applications related to both the fields of security and cyber-physical systems.

Invited Speakers

Tachio Terauchi: Constraint-based relational verification (recording; slides)
Waseda University, Japan

Tachio Terauchi is a professor in the Department of Computer Science and Engineering at Waseda University. He received his M.S. and Ph.D. from University of California Berkeley in 2004 and 2006, and B.S. from Columbia University in 2000, all in computer science. Before joining Waseda, he was a professor at JAIST from 2014 to 2017, an associate professor at Nagoya University from 2011 to 2014, and an assistant professor at Tohoku University from 2007 to 2011. Terauchi is interested in techniques for building reliable computational systems. His work draws from, and contributes to the areas of programming languages, program analysis, program verification, program synthesis, type systems, mathematical logic, automated deduction, and security.

Orna Grumberg: Compositional model checking for multi-properties (recording)
Technion, Israel

Orna Grumberg is a Professor in the Computer Science Department at the Technion. She is a member of the Academia Europaea and an ACM fellow. She holds a Ph.D. from the Computer Science Department at the Technion, and an Honorary Doctorate from the Technical University of Munich. Grumberg serves on the steering committee of the main conference on model checking - Computer-aided Verification (CAV). She serves on numerous program committees of leading conferences and on the editorial boards of two of the main journals in her field. Grumberg is the co-author of the highly cited book "Model Checking", which is a main reference in the field of Formal Verification. Her work is published in leading conferences and is widely cited. Her work on counterexample-guided abstraction refinement (CEGAR) has won the CAV award.

Bernd Finkbeiner: Probabilistic Hyperproperties of Markov Decision Processes (recording)
CISPA Helmholtz Center for Information Security, Germany

Bernd Finkbeiner is a faculty member at the CISPA Helmholtz Center for Information Security and a professor for computer science at Saarland University. He obtained his Ph.D. in 2003 from Stanford University. Since 2003, he leads the Reactive Systems Group, which became part of CISPA in 2020. His research focus is the development of reliable guarantees for the safety and security of computer systems, including specification, program synthesis and repair, and static and dynamic verification.

Sanjit A. Seshia: Formal Specification for Machine Learning Systems (recording; slides)
University of California, Berkeley, USA

Sanjit A. Seshia is a Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in formal methods for dependable and secure computing, with a current focus on the areas of cyber-physical systems, computer security, machine learning, and robotics. He has made pioneering contributions to the areas of satisfiability modulo theories (SMT), SMT-based verification, and inductive program synthesis. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, the Donald O. Pederson Best Paper Award for the IEEE Transactions on CAD, and the IEEE Technical Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award. He is a Fellow of the ACM and the IEEE.

Jyotirmoy V. Deshmukh: Trust-aware Control for Multi-Agent Systems: a future arena for hyperproperties? (recording; slides)
University of Southern California, USA

Jyotirmoy V. Deshmukh is an assistant professor in the Department of Computer Science at the University of Southern California in Los Angeles, USA. Before joining USC, Jyo worked as a Principal Research Engineer in Toyota R&D. He received his Ph.D. degree from the University of Texas at Austin and was a post-doctoral fellow at the University of Pennsylvania. Dr. Deshmukh's research interest is in the broad area of analysis, design, security and trustworthiness, and synthesis of cyber-physical systems, including those that use machine learning and AI-based components.

Borzoo Bonakdarpour: Controller Synthesis for Hyperproperties (recording; slides)
Michigan State University, USA

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 90 articles and papers in top journals and conferences. His work in these areas have received multiple best paper awards from highly prestigious conferences, including, SRDS'17, SSS'14, and SIES'10. He chaired the Technical Program Committee of the SRDS'20, SSS'16, and RV'14 conferences.


Monday, October 18, 2021; all times are in PDT (UTC-7).

7:00 Welcome
7:15 Tachio Terauchi (recording; slides)
Constraint-based relational verification
8:00 Orna Grumberg (recording)
Compositional model checking for multi-properties
8:45 Break
9:00 Bernd Finkbeiner (recording)
Probabilistic Hyperproperties of Markov Decision Processes
9:45 Sanjit A. Seshia (recording; slides)
Formal Specification for Machine Learning Systems
10:30 Break
10:45 Jyotirmoy V. Deshmukh (recording; slides)
Trust-aware Control for Multi-Agent Systems: a future arena for hyperproperties?
11:30 Borzoo Bonakdarpour (recording; slides)
Controller Synthesis for Hyperproperties
12:15 Break
12:30 Panel discussion (recording)
13:15 End


Please register via the ATVA registration site. Note that workshop-only registration is free.


Recordings of the HYPER 2021 talks and panel discussion are available on YouTube.


  • Daniel Fremont, University of California, Santa Cruz
  • Hazem Torfah, University of California, Berkeley