POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Fri 19 Jan 2024 17:10 - 17:30 at Turing Lecture - Logical Foundations Chair(s): Emanuele D’Osualdo

We introduce a novel logic for asynchronous hyperproperties with a new mechanism to identify relevant positions on traces. While the new logic is more expressive than a related logic presented recently by Bozzelli et al., we obtain the same complexity of the model checking problem for finite state models. Beyond this, we study the model checking problem of our logic for pushdown models. We argue that the combination of asynchronicity and a non-regular model class studied in this paper constitutes the first suitable approach for hyperproperty model checking against recursive programs.

Fri 19 Jan

Displayed time zone: London change

16:50 - 17:50
Logical FoundationsPOPL at Turing Lecture
Chair(s): Emanuele D’Osualdo MPI-SWS
16:50
20m
Talk
Orthologic with Axioms
POPL
Simon Guilloud École Polytechnique Fédérale de Lausanne, Viktor Kunčak EPFL, Switzerland
Pre-print
17:10
20m
Talk
Deciding Asynchronous Hyperproperties for Recursive Programs
POPL
Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-Olm University of Münster, Christoph Ohrem University of Münster
Pre-print
17:30
20m
Talk
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
POPL
Patrick Cousot New York University