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.
• The semantic approach highlights essential concepts without syntactic overhead, and simplifies soundness and completeness proofs • A detailed introduction to compositional proof methods each of which is proved to be sound and (semantically) complete • Every method is illustrated by many examples, and a picture gallery of key figures complements the text
Contents
Preface; Part I. Introduction and Overview: 1. Introduction; Part II. The Inductive Assertion Method: 2. Floyd's inductive assertion method for transition diagrams; 3. The inductive assertion method for shared-variable concurrency; 4. The inductive assertion method for synchronous message passing; 5. Expressibility and relative completeness; Part III. Compositional Proof Methods: 6. Introduction to compositional reasoning; 7. Compositional proof methods: synchronous message passing; 8. Compositional proof methods: shared-variable concurrency; Part IV. Hoare Logic: 9. A proof system for sequential programs using Hoare triples; 10. A Hoare logic for shared-variable concurrency; 11. A Hoare logic for synchronous message passing; Part V. Layered Design: 12. Transformational design and Hoare logic; Bibliography; Glossary of symbols; Index.
Review
'The present textbook is a highly welcome addition to the existing literature on program verification, particularly valuable for the well-arranged, methodically unified framework for a wealth of material.' Zentralblatt für Mathematik und ihre Grenzgebiete Mathematics Abstracts
Printer friendly version
Email a colleague