@inproceedings{a0e532eab7594108b959466450ad76cd,
title = "Petrification: Software Model Checking for Programs with Dynamic Thread Management",
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.",
keywords = "Concurrency, Fork-Join, Petri Nets, Verification, pthreads",
author = "Matthias Heizmann and Dominik Klumpp and Lars Nitzke and Frank Sch{\"u}ssele",
note = "Publisher Copyright: {\textcopyright} 2024, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 25th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2024 was co-located with 51st ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2024 ; Conference date: 15-01-2024 Through 16-01-2024",
year = "2024",
month = jan,
day = "1",
doi = "10.1007/978-3-031-50521-8\_1",
language = "English",
isbn = "9783031505201",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "3--25",
editor = "Rayna Dimitrova and Ori Lahav and Sebastian Wolff",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings",
}