Limit search to available items
Book Cover

Title Handbook of model checking / Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem, editors
Published Cham, Switzerland : Springer, 2018
Online access available from:
Springer eBooks    View Resource Record  


Description 1 online resource (xxiv, 1210 pages) : illustrations (some color)
Contents Intro; Handbook of Model Checking; Foreword; Preface; Acknowledgements; Contents; Contributors; Chapter 1: Introduction to Model Checking; 1.1 The Case for Computer-Aided Veri cation; 1.2 Temporal-Logic Model Checking in a Nutshell; 1.2.1 Kripke Structures; 1.2.2 The Temporal Logic CTL; 1.2.3 The Temporal Logic CTL; 1.2.4 The Temporal Logic LTL; 1.3 A Very Brief Guide Through the Chapters of the Handbook; 1.3.1 The Algorithmic Challenge; 1.3.2 The Modeling Challenge; 1.4 The Future of Model Checking; References; Chapter 2: Temporal Logic and Fair Discrete Systems; 2.1 Introduction
2.2 Fair Discrete Systems2.2.1 Kripke Structures; 2.2.2 De nition of Fair Discrete System; 2.2.3 Representing Programs; 2.2.4 Algorithms; 2.3 Linear Temporal Logic; 2.3.1 De nition of Linear Temporal Logic; 2.3.2 Safety Versus Liveness and the Temporal Hierarchy; 2.3.3 Extensions of LTL; 2.3.4 Temporal Testers, Satis ability, and Model Checking; 2.4 Computation Tree Logic; 2.4.1 De nition of Computation Tree Logic; 2.4.2 Extensions; 2.4.3 Model Checking and Satis ability; 2.5 Examples for LTL and CTL; 2.5.1 Invariance and Safety; 2.5.2 Liveness; 2.5.3 Additional Examples; 2.6 CTL*
2.6.1 Branching vs. Linear Time2.6.2 CTL* De nition; 2.6.3 Examples of Usage of CTL*; 2.6.4 Model Checking and Satis ability; References; Chapter 3: Modeling for Veri cation; 3.1 Introduction; 3.2 Major Considerations in System Modeling; 3.2.1 Selecting a Modeling Formalism and Language; Type of System; Type of Property; Modeling the Environment; Level of Abstraction; Clarity and Modularity; Form of Composition; Computational Engines; Practical Ease of Modeling and Expressiveness; 3.2.2 Modeling Languages
3.2.3 Challenges in Modeling3.2.4 Scope of This Chapter; 3.3 Modeling Basics; 3.3.1 Syntax; 3.3.2 Dynamics; 3.3.3 Modeling Concepts; 3.4 Examples; 3.4.1 Synchronous Circuits; Router Design; Simpli cations and sml Model; Veri cation Task: Progress Through the Router; Data Type Abstraction; Environment Modeling; Summary; 3.4.2 Synchronous Control Systems; 3.4.3 Concurrent Software; 3.5 Kripke Structures; 3.5.1 Transition Systems; 3.5.2 From sml Programs to Kripke Structures; 3.6 Summary; References; Chapter 4: Automata Theory and Model Checking
4.1 Introduction4.2 Nondeterministic B├╝chi Automata on In nite Words; 4.2.1 De nitions; 4.2.2 Closure Properties; Closure Under Union and Intersection; Closure Under Complementation; 4.2.3 Determinization; 4.3 Additional Acceptance Conditions; 4.3.1 Translations Among the Different Classes; Translations Among the Different Conditions; Typeness; Translations That Require a New State Space; 4.3.2 Determinization of NBWs; 4.4 Decision Procedures; 4.5 Alternating Automata on In nite Words; 4.5.1 De nition; 4.5.2 Closure Properties; 4.5.3 Decision Procedures
Summary Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry. The editors and authors of this handbook are among the world's leading researchers in this domain, and the 32 contributed chapters present a thorough view of the origin, theory, and application of model checking. In particular, the editors classify the advances in this domain and the chapters of the handbook in terms of two recurrent themes that have driven much of the research agenda: the algorithmic challenge, that is, designing model-checking algorithms that scale to real-life problems; and the modeling challenge, that is, extending the formalism beyond Kripke structures and temporal logic. The book will be valuable for researchers and graduate students engaged with the development of formal methods and verification tools. "This handbook is an authoritative, comprehensive description of the state of the art in model checking. It belongs on the bookshelf of every researcher and practitioner in computer-aided verification." [Moshe Y. Vardi, George Distinguished Service Professor in Computational Engineering, Rice University] "With chapters written by the world's leading experts from academia and industry, this authoritative book on model checking should be on the shelf of every computer science graduate student and every hardware and software engineer. As the scale and complexity of digital systems grow, and they must work in the presence of uncertainty in the physical world, verification techniques such as model checking will become increasingly important to ensure system reliability, safety, and security." [Jeannette Wing, Corporate Vice President, Microsoft Research]
Bibliography Includes bibliographical references
Notes Online resource; title from PDF title page (SpringerLink, viewed May 21, 2018)
Subject Computer systems -- Verification -- Handbooks, manuals, etc.
Genre/Form Handbooks and manuals.
Handbooks and manuals.
Form Electronic book
Author Bloem, Roderick P., editor
Clarke, Edmund M., Jr. (Edmund Melson), 1945- editor
Henzinger, T. A. (Thomas A.), editor
Veith, Helmut, editor
ISBN 3319105752 (electronic bk.)
9783319105758 (electronic bk.)