POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

Dynamic Pushdown Networks (DPNs) are a model for multithreaded programs with recursion and dynamic creation of threads. In this paper, we propose a temporal logic called NTL for reasoning about the call- and return- as well as thread creation behaviour of DPNs. Using tree automata techniques, we investigate the model checking problem for the novel logic and show that its complexity is not higher than that of LTL model checking against pushdown systems despite a more expressive logic and a more powerful system model. The same holds true for the satisfiability problem when compared to the satisfiability problem for a related logic for reasoning about the call- and return-behaviour of pushdown systems. Overall, this novel logic offers a promising approach for the verification of recursive programs with dynamic thread creation.

Tue 16 Jan

Displayed time zone: London change

16:00 - 17:30
Session 8: Concurrency, Program and System Verification, ClosingVMCAI at Marconi Room
Chair(s): Viktor Kunčak EPFL, Switzerland
16:00
20m
Talk
Petrification: Software Model Checking for Programs with Dynamic Thread Management
VMCAI
Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Lars Nitzke University of Freiburg, Frank Schüssele University of Freiburg
Pre-print
16:20
20m
Talk
A Fully Verified Persistency Library
VMCAI
Stefan Bodenmüller University of Augsburg, John Derrick , Brijesh Dongol University of Surrey, Gerhard Schellhorn Universitaet Augsburg, Heike Wehrheim University of Oldenburg
16:40
20m
Talk
A Navigation Logic for Recursive Programs with Dynamic Thread Creation
VMCAI
Roman Lakenbrink University of Münster, Markus Müller-Olm University of Münster, Christoph Ohrem University of Münster, Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany
Pre-print
17:00
20m
Talk
Borrowable Fractional Ownership Types for Verification
VMCAI
Takashi Nakayama The University of Tokyo, Yusuke Matsushita The University of Tokyo, Ken Sakayori University of Tokyo, Ryosuke Sato University of Tokyo, Naoki Kobayashi University of Tokyo
Pre-print
17:20
10m
Day closing
Closing (+ best paper award announcement)
VMCAI