A Navigation Logic for Recursive Programs with Dynamic Thread Creation
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 JanDisplayed 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 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | 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 10mDay closing | Closing (+ best paper award announcement) VMCAI |