Petrification: Software Model Checking for Programs with Dynamic Thread Management (VMCAI 2024)

Sun 14 - Sat 20 January 2024 London, United Kingdom

Who

Matthias Heizmann, Dominik Klumpp, Lars Nitzke, Frank Schüssele

Track

VMCAI 2024

Time Zone

The program is currently displayed in (GMT) London.

Use conference time zone: (GMT) LondonSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 16 Jan 2024 16:00 - 16:20 at Marconi Room - Session 8: Concurrency, Program and System Verification, Closing Chair(s): Viktor Kunčak

Abstract

We address the verification problem for concurrent program that dynamically create (fork) new threads or destroy (join) existing threads. We present a reduction to the verification problem for concurrent programs with a fixed number of threads. More precisely, we present petrification, a transformation from programs with dynamic thread management to an existing, Petri net-based formalism for programs with a fixed number of threads. Our approach is implemented in a software model checking tool for C programs that use the pthreads API.

Link to Preprint

https://arxiv.org/abs/2311.01302

Matthias Heizmann

University of Freiburg, Germany

Germany

Dominik Klumpp

University of Freiburg

Germany

Lars Nitzke

University of Freiburg

Germany

Frank Schüssele

University of Freiburg

Germany

Time Zone

The program is currently displayed in (GMT) London.

Use conference time zone: (GMT) LondonSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

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