Petrification: Software Model Checking for Programs with Dynamic Thread Management (Extended Version)
Programming Languages
2023-11-03 v1
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.
Cite
@article{arxiv.2311.01302,
title = {Petrification: Software Model Checking for Programs with Dynamic Thread Management (Extended Version)},
author = {Matthias Heizmann and Dominik Klumpp and Frank Schüssele and Lars Nitzke},
journal= {arXiv preprint arXiv:2311.01302},
year = {2023}
}
Comments
32 pages, 8 figures, 2 tables, extended version of the paper which is to appear at VMCAI 2024