A practical guide to proving correctness in parallel programs with automated verification.
This book presents a concrete approach to verifying compact parallel coordination programs. It introduces how auxiliary state, like counters and control variables, can be used to analyze dynamic behavior and prove properties for arbitrary numbers of processing elements. Through worked examples, the text shows how verification tools describe reachability and correctness for complex parallel systems.
- Learn how to model parallel programs with state spaces and metastates
- See how reachability descriptions and invariant assertions support proofs
- Explore real examples like readers-writers and semaphore-like synchronization
- Understand how automated verifiers generate compact proofs that hold for any number of processors
Ideal for readers of formal methods, concurrency theory, and practical verification of parallel software.