PLDI 2024
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark
Tue 25 Jun 2024 11:13 - 11:46 at Helsinki - Session 2

(joint work with Bernd Finkbeiner)

Hyperproperties are system properties that relate multiple traces (executions) of a system. Typical applications of hyperproperties are found in information flow security. Previously, we introduced concurrent hyperproperties, by generalizing traces to concurrent traces, defined as partially ordered multisets. We take Petri nets as the basic semantic model. To check concurrent hyperproperties, we extended the testing of processes due to De Nicola and Hennessy to the setting of concurrent traces, using the parallel composition of Petri nets. We present new results on decidability and undecidability of may and must testing of universal and existential concurrent hyperproperties, and analyze the case of concurrent hyperproperties with quantifier alternation.

Tue 25 Jun

Displayed time zone: Windhoek change

10:40 - 12:20
Session 2PODELSKI at Helsinki
10:40
33m
Talk
Session Types for People who Love Automata
PODELSKI
Thomas Wies New York University
11:13
33m
Talk
Concurrent ∀∃-Hyperproperties
PODELSKI
Ernst-Rüdiger Olderog University of Oldenburg
11:46
33m
Talk
Optimal Quantum Programs
PODELSKI
Jens Palsberg University of California, Los Angeles (UCLA)