Concurrency Verification: Introduction to Compositional and Non-compositional Methods
Book information
Description
This is a systematic and comprehensive introduction both to compositional proof methods for the state-based verification of concurrent programs, such as the assumption-commitment and rely-guarantee paradigms, and to noncompositional methods, whose presentation culminates in an exposition of the communication-closed-layers (CCL) paradigm for verifying network protocols. Compositional concurrency verification methods reduce the verification of a concurrent program to the independent verification of its parts. If those parts are tightly coupled, one additionally needs verification methods based on the causal order between events. These are presented using CCL. The semantic approach followed here allows a systematic presentation of all these concepts in a unified framework which highlights essential concepts. The book is self-contained, guiding the reader from advanced undergraduate level to the state-of-the-art. Every method is illustrated by examples, and a picture gallery of some of the subject's key figures complements the text.
Similar books
Software Engineering and Formal Methods: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings
2020 · PDF
It's All About Coordination
2018 · PDF
Compositionality: The Significant Difference: International Symposium, COMPOS’97 Bad Malente, Germany, September 8–12, 1997 Revised Lectures
1998 · PDF
Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems: Joint International Conferences on Formal Modeling and Analysis of Timed Systmes, FORMATS 2004, and Formal Techniques in Real-Time and Fault -Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004. Proceedings
2004 · PDF
Fundamentals of Software Engineering: 5th International Conference, FSEN 2013, Tehran, Iran, April 24-26, 2013, Revised Selected Papers
2013 · PDF
Formal Methods for Components and Objects: Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2-5, 2004, Revised Lectures ... / Programming and Software Engineering)
2005 · PDF
Data Refinement: Model-Oriented Proof Methods and their Comparison
2008 · PDF
Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems: Joint International Conferences on Formal Modeling and Analysis of Timed Systmes, FORMATS 2004, and Formal Techniques in Real-Time and Fault -Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004. Proceedings
2004 · PDF