3rd Workshop on Hyperproperties: Advances in Theory and Applications
23 July @ CAV 2024
Montreal, Canada
The study of hyperproperties has recently gained a great deal of attention in the formal methods, security, and cyber-physical systems communities. They have become a widely-used formalism for expressing system properties such as information-flow policies, symmetry in hardware design, robustness in cyber-physical systems, as well as properties of learning-enabled systems. The goal of this workshop 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 formalisms and methods for specifying and analyzing hyperproperties. Topics of interest include, but are not limited to, developments on logical formalisms for specifying hyperproperties, algorithmic methodologies for the verification, synthesis, and runtime verification of hyperproperties, as well as applications related to the fields of cyber-physical systems, security and machine learning.
Invited Speakers
Fred Schneider
Cornell, USA
Fred B. Schneider has been on Cornell's faculty since 1978. He is
known for his research in trustworthy systems, spanning fault-tolerant
distributed systems, formal methods, and cybersecurity. He is author
of two formal methods textbooks: "Logical Approach to Discrete Math"
(co-authored with David Gries) and "On Concurrent Programming". And
along with Bowen Alpern he devised the now standard formal definition
of "liveness properties" along with a proof that safety and liveness
are a fundamental basis for all trace-properties; that work received
the 2018 Edsger W. Dijkstra Prize in Distributed Computing. Schneider
is a member of the US National Academy of Engineering and the American
Academy of Arts & Sciences; he is a foreign member of the Norges
Tekniske Vitenskapsakademi (Norwegian Academy of Technological
Sciences).
Hagit Attiya
Technion, Israel
Hagit Attiya is a professor at the department of Computer Science at the Technion,
Israel Institute of Technology, and holds the
Harry W. Labov and Charlotte Ullman Labov Academic Chair.
She is the editor-in-chief of Springer's journal Distributed Computing.
She won the Dijkstra award in Distributed Computing 2011 and is a fellow of the ACM.
She received all her academic degrees, in Computer Science, from the Hebrew University
of Jerusalem, and was a post-doctoral fellow at MIT.
Jana Hofmann
Azure Reserach, UK
Jana Hofmann is a researcher at Azure Research, Microsoft. She obtained her PhD in 2022 at CISPA/Saarland University, for which she received the university’s Dr.-Eduard-Martin Prize for best computer science thesis of the year. She develops logics, formal methods, and testing techniques for hyperproperties. In particular, she works on principled methods to detect, model, and prevent information leakage through microarchtectural side channels.
Xiang Yin
Shanghai Jiao Tong University, China
Xiang Yin received the B.Eng degree from Zhejiang University in 2012, the M.S. degree from the University of Michigan, Ann Arbor, in 2013, and the Ph.D degree from the University of Michigan, Ann Arbor, in 2017, all in electrical engineering. Since 2017, he has been with the Department of Automation, Shanghai Jiao Tong University, where he is an Associate Professor. His research interests include formal methods, discrete-event systems and cyber-physical systems. Dr. Yin is serving as the chair of the IEEE CSS Technical Committee on Discrete Event Systems, an Associate Editor for the Journal of Discrete Event Dynamic Systems: Theory & Applications, and a member of the IEEE CSS Conference Editorial Board. Dr. Yin received the IEEE Conference on Decision and Control (CDC) Best Student Paper Award Finalist in 2016.
Call for Presentations
The HYPER workshop aims to bring together researchers interested in the broad area of hyperproperties and working in the areas of formal methods and control, cybersecurity, and machine learning. HYPER 2024 is co-located with CAV 2024, and will take place in Montreal, Canada, on July 23, 2024. Topics of interest include, but are not limited to:
Specification formalisms for hyperproperties
Algorithms for verification, synthesis, and runtime verification for hyperproperties
Information-flow control
Privacy
Fairness
Causality
Robustness
Explainability
Presentation proposals shall be submitted in form of an extended abstract of up to three pages in LNCS format (not including references) via the easychair link https://easychair.org/my/conference?conf=hyper24. Submissions can overlap with previously published work and will be judged based on their relevance to the topic of the workshop. The review process will be single blind and the deadline for submission is May 16, 2024 AoE.
Selected submissions will be invited for a topical collection on Hyperproperties at Acta Informatica.
