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

2023/11/02 by Matthias Heizmann, Heizmann, Matthias, Dominik Klumpp +5
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Petri Nets in System Modeling #Programming Languages (cs.PL) #Service-Oriented Architecture and Web Services

paper · pdf · doi:10.48550/arxiv.2311.01302

openalex publication_date 2023/11/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• Modular Verification of Concurrent Programs via Sequential Model Checking
• Constraint-based automatic verification of abstract models of multithreaded programs
• Program Dependence Net and On-demand Slicing for Property Verification of Concurrent System and Software
• Constraint-based verification of abstract models of multitreaded programs
• Dynamic partial-order reduction for model checking software