Concurrency verification. Introduction to compositional and noncompositional methods (Q2768503)

This textbook is the first part of a work published in two volumes devoted to the state-based verification of concurrent programs. In the first chapter the authors advocate by means of 3 examples the need to use (semi-) automated proof checkers to eliminate errors in verification proofs and explain the approach taken in this volume: state-based, property-oriented, dual language, and semantically-oriented. NEWLINENEWLINENEWLINEIn Chapter 2 semantical formulation is introduced of Floyd's inductive assertion method for sequential transition systems. This simple model of sequential programming is generalised in the next 2 chapters to, respectively, shared-variable concurrency and to distributed programs communicating by means of synchronous messages. The focus is on formulating a mathematical basis for state-based program verification and on proving partial correctness, absence of deadlock, absence of runtime errors, and termination properties. All proposed verification methods are proved to be sound and semantically complete. The goal of Chapter 5 is to investigate the expressibility of mathematical entities used in the soundness and semantic completeness proofs of the previous chapters in the language of first-order predicate logic over the standard model of the natural numbers. This result allows the authors to carry these proofs from the semantic level to the syntactic level of Hoare logic and constitutes in the opinion of the authors ``one of the distinguishing methodological features of this book''. Compositional reasoning on large programs, understood as a strategy to verify a program ``on the basis of the specifications of its constituent subprograms only, without any knowledge of the interior construction of those subprograms'' is introduced in Chapter 6. This principle is very attractive for application to parallel composition because the complexity of this reasoning increases linearly w.r.t. the number of parallel components. The next two chapters are devoted to two powerful paradigms for compositional reasoning: the assumption-commitment method for verifying synchronous distributed message passing system and the rely-guarantee method for verifying shared-variable concurrency. NEWLINENEWLINENEWLINEIn Chapters 9-11 it is given a broad interpretation of Hoare logic regarded as a structured proof method for the inductive construction of inductive assertion networks for programs. Hoare-style proof systems for sequential programs, for shared-variable concurrency, and for synchronous message passing are formulated. Soundness and relative completeness of these logics is immediately derived from results previously obtained. The last chapter of the book explains how to develop a concurrent program starting from a relatively simple version of it, proving this basic instance is correct, and then transforming the sequential version into the actual program. Several program-transforms (including the communication-closed-layers paradigm for verifying network protocols) based on linear time temporal logic are introduced and proved correct. NEWLINENEWLINENEWLINEAll chapters end with exercises of various degrees of difficulty; the hardest ones and the open problems are marked as such. Ample historical notes serve as annotations for the more than 650 references listed in the bibliography. Every method is illustrated by examples explained at length. The formal exposition of essential ideas is preceded by informal discussions. The proofs are clear, detailed, and accompanied by enlightening comments. NEWLINENEWLINENEWLINEThe material contained in this textbook has been already used for courses of various duration. It is partly accessible for undergraduate students. Many themes appear for the first time in a self-contained textbook. More technical sections are aimed to lead up to state-of-the-art research in the area of compositional methods for concurrent program verification. 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.