Petrification: Software Model Checking for Programs with Dynamic Thread Managem...
summary
Petrification reduces C programs using pthread_create/pthread_join to a fixed-N, 1-safe Petri net model and iteratively increases N until the modeled thread width suffices; it encodes fork by moving a token from not_inuse to inuse and encodes join by matching an ID variable and removing that token. Implementation targets Ultimate Tools Jem cutter automizer and typon, checks safety assertions only, is complete for programs with finite thread width, and succeeds on the reported benchmark suite whenever the underlying Petri-net verifier terminates.
AI-written summary · about
chapters (6)
- 0:00Petrification introduction
- 2:40Dynamic thread management
- 5:27Thread width challenges
- 7:16Modeling with Petri Nets
- 13:22Ultimate tools challenges
- 14:28Conclusion
related talks
43mMultithreading for human beings
05mProgramming with Petri Nets to Reason about Concurrency (Lightning Talk)
01h 41mThreads Considered Harmful
55mJava PathFinder: going to Mars without bugs and deadlocks
26mContext-Bounded Verification of Liveness for Multithreaded Shared-Memory Programs
37mEverything you ever wanted to know about threads...
19mPete's Footprints
22mContext-Bounded Verification of Thread Pools