+612 9045 4394
Cambridge Tracts in Theoretical Computer Science : Concurrency Verification: Introduction to Compositional and Non-compositional Methods Series Number 54 - Willem-Paul de Roever

Cambridge Tracts in Theoretical Computer Science

Concurrency Verification: Introduction to Compositional and Non-compositional Methods Series Number 54

Paperback Published: 26th January 2012
ISBN: 9780521169325
Number Of Pages: 800

Share This Book:


RRP $121.95
or 4 easy payments of $24.81 with Learn more
This title is not in stock at the Booktopia Warehouse and needs to be ordered from our supplier.
Click here to read more about delivery expectations.

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.

Review of the hardback: '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 fur Mathematik und ihre Grenzgebiete Mathematics Abstracts
"It is capable of replacing a multitude of original articles...with one coherent text. Wherever appropriate, however, the book does refer in detail to original research, and includes many historical hints. It also provides a rich choice of exercises." Computing Reviews
"The book gives a very comprehensive presentation of what we know so far about proving concurrent systems...It gives an excellent survey of the field and lots of examples and technical details." Mathematical Reviews

Prefacep. ix
Introduction and Overviewp. 1
Introductionp. 2
Central Questionsp. 2
Structure of this Chapterp. 2
Basic Concepts of Concurrencyp. 3
Why Concurrent Programs Should be Proved Correctp. 8
The Approach of this Bookp. 33
Compositionalityp. 46
From Noncomp. to Comp. Proof Methods - a historical perspectivep. 62
The Inductive Assertion Methodp. 71
Floyd's Inductive Assertion Method for Transition Diagramsp. 72
Objectives of Part IIp. 72
Structure of this Chapterp. 75
Sequential Transition Diagrams and Systemsp. 76
Specification and Correctness Statementsp. 82
A Proof Method for Partial Correctnessp. 88
Soundnessp. 92
Semantic Completeness of the Inductive Assertion Methodp. 93
Proving Convergencep. 98
Proving Absence of Runtime Errorsp. 104
Historical Notesp. 111
The Inductive Assertion Method for Shared-Variable Concurrencyp. 119
Objective and Structure of this Chapterp. 119
A Characterisation of Concurrent Executionp. 121
Is this Characterisation of Concurrent Execution Justified?p. 132
The Generalisation of Floyd's Approach to Nondeterministic Interleavingsp. 134
Concurrent Transition Systems with Shared Variablesp. 137
Proving Convergence for Shared-Variable Concurrencyp. 188
Proving Deadlock Freedomp. 203
Proving Absence of Runtime Errorsp. 206
Historical Notesp. 208
The Inductive Assertion Method for Synchronous Message Passingp. 221
Objective and Introductionp. 221
Structure of this Chapterp. 223
Syntax and Semantics of Synchronous Transition Diagramsp. 223
Proof Methods for Partial Correctnessp. 227
Semantic Completenessp. 249
Technical Note: Modifications Towards Compositionalityp. 264
A Modular Method for Proving Convergencep. 269
Verifying Deadlock Freedomp. 277
Proving Absence of Runtime Errorsp. 279
Historical Notesp. 282
Expressibility and Relative Completenessp. 291
Objectivep. 291
Structure of this Chapterp. 292
Syntactic Notionsp. 292
Partial Correctness of Syntactic Transition Diagramsp. 298
Relative Completeness of Floyd's Inductive Assertion Methodp. 300
Relative Completeness of the Method of Owicki & Griesp. 309
Relative Completeness of the Method of Apt, Francez & de Roeverp. 312
Historical Notesp. 316
Picture Galleryp. 319
Compositional Methods based on Assertion Networksp. 353
Introduction to Compositional Reasoningp. 354
Motivationp. 354
Introduction to Part III and to this Chapterp. 356
Assume-Guarantee-based Reasoningp. 359
Assumption-Commitment-based Reasoningp. 361
Rely-Guarantee-based Reasoningp. 363
Compositional Proof Methods: Synchronous Message Passingp. 367
Objective and Introductionp. 367
Structure of the Chapterp. 368
Top-level Synchronous Message Passingp. 369
A Compositional Proof Method for Nested Parallelismp. 379
Assumption-Commitment-based Reasoningp. 397
Historical Notesp. 429
Compositional Proof Methods: Shared-Variable Concurrencyp. 438
Introduction and Overviewp. 438
Concurrent Transition Diagramsp. 439
Top-Level Shared-Variable Concurrencyp. 440
The Rely-Guarantee Methodp. 447
Historical Notesp. 479
Hoare Logicp. 487
A Proof System for Sequential Programs Using Hoare Triplesp. 488
Introduction and Overview of Hoare Logicsp. 488
Structure of this Chapterp. 497
Syntax and Informal Meaning of GCL+ Programsp. 498
Semantics of GCL+p. 501
A Proof System for GCL+ Programsp. 506
Soundness and Relative Completenessp. 511
Proof Outlinesp. 517
Alternative Definitions of Proof Outlinesp. 521
Examples of Verification during Program Developmentp. 522
Historical Notesp. 526
A Hoare Logic for Shared-Variable Concurrencyp. 531
Introduction and Overviewp. 531
Syntax and Informal Meaning of SVL Programsp. 532
Semantics of SVL+p. 537
A Proof System for SVL Programsp. 540
An Extended Example: Concurrent Garbage Collectionp. 563
Completeness of the Owicki & Gries Methodp. 584
A Hoare Logic for Synchronous Message Passingp. 600
Structure of this Chapterp. 600
Syntax and Informal Meaning of DML Programsp. 601
Semantics of DMLp. 606
A Hoare Logic for Synchronous Message Passingp. 608
Soundness and Relative Completeness of this Hoare Logicp. 630
Technical Note: Modifications Towards Compositionalityp. 638
Layered Designp. 653
Transformational Design and Hoare Logicp. 654
Introduction and Overviewp. 654
Structure of this Chapterp. 660
Syntax and Informal Meaning of SVL++ Programsp. 660
The Semantics of SVL++ Programsp. 662
Partial Orders and Temporal Logicp. 663
The Communication-Closed-Layers Lawsp. 676
The Two-Phase Commit Protocolp. 688
Assertion-Based Program Transformationsp. 694
Loop Distributionp. 696
Set-partitioning Revisitedp. 700
Historical Notesp. 704
Bibliographyp. 710
Glossary of Symbolsp. 747
Indexp. 761
Table of Contents provided by Ingram. All Rights Reserved.

ISBN: 9780521169325
ISBN-10: 0521169321
Series: Cambridge Tracts in Theoretical Computer Science (Paperback)
Audience: Tertiary; University or College
Format: Paperback
Language: English
Number Of Pages: 800
Published: 26th January 2012
Country of Publication: GB
Dimensions (cm): 22.86 x 15.24  x 4.04
Weight (kg): 1.05