Petrification: Software Model Checking for Programs with Dynamic Thread Management (Extended Version)

Autor:	Heizmann, Matthias, Klumpp, Dominik, Schüssele, Frank, Nitzke, Lars
Rok vydání:	2023
Předmět:	Computer Science - Programming Languages
Druh dokumentu:	Working Paper
Popis:	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. Comment: 32 pages, 8 figures, 2 tables, extended version of the paper which is to appear at VMCAI 2024
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2311.01302 Zobrazit plný text záznamu View this record from Arxiv