Willem-Paul de Roever, Frank de Boer, Jozef Hooman

Concurrency Verification

Introduction to Compositional and Non-Compositional Methods

• Gebundenes Buch

Produktbeschreibung

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.

Table of 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.

This is the first introduction to verifying concurrent programs scaling up to a realistic size. It is self-contained and comprehensive, 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.

Advanced textbook on verification of concurrent programs using a semantic approach which highlights concepts clearly.

---

Hinweis: Dieser Artikel kann nur an eine deutsche Lieferadresse ausgeliefert werden.

Produktdetails

• Verlag: Cambridge University Press
• Seitenzahl: 800
• Erscheinungstermin: 10. August 2011
• Englisch
• Abmessung: 235mm x 157mm x 47mm
• Gewicht: 1288g
• ISBN-13: 9780521806084
• ISBN-10: 0521806089
• Artikelnr.: 22400355

Inhaltsangabe

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.