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

Matthias Heizmann, Dominik Klumpp, Frank Schüssele +1

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…