Petrification: Software Model Checking for Programs with Dynamic Thread Management

Petrification: Software Model Checking for Programs with Dynamic Thread Management

Explore a conference talk on software model checking for programs with dynamic thread management. Delve into the concept of petrification, a novel approach that transforms programs with dynamic thread creation and destruction into a Petri net-based formalism for fixed-thread programs. Learn how this method addresses the verification problem for concurrent programs using dynamic thread management. Discover the implementation of this approach in a software model checking tool for C programs utilizing the pthreads API. Gain insights from speakers Matthias Heizmann, Dominik Klumpp, Lars Nitzke, and Frank Schüssele as they present their research findings at the VMCAI'24 conference.