Handbook of Model Checking

• Corporate Author: SpringerLink (Online service)
• Other Authors: Clarke, Edmund M. (Editor, http://id.loc.gov/vocabulary/relators/edt), Henzinger, Thomas A. (Editor, http://id.loc.gov/vocabulary/relators/edt), Veith, Helmut (Editor, http://id.loc.gov/vocabulary/relators/edt), Bloem, Roderick (Editor, http://id.loc.gov/vocabulary/relators/edt)
• Format: Electronic eBook
• Language: English
• Published: Cham : Springer International Publishing : Imprint: Springer, 2018.
• Edition: 1st ed. 2018.
• Subjects: Computers.; Software engineering.; Mathematical logic.; Computer science-Mathematics.; Computer software-Reusability.; Quality control.; Reliability.; Industrial safety.; Theory of Computation.; Software Engineering/Programming and Operating Systems.; Mathematical Logic and Foundations.; Mathematics of Computing.; Performance and Reliability.; Quality Control, Reliability, Safety and Risk.

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

Table of Contents:

• Introduction to Model Checking
• Temporal Logic and Fair Discrete Systems
• Modeling for Verification
• Automata Theory and Model Checking
• Explicit-State Model Checking
• Partial-Order Reduction
• Binary Decision Diagrams
• BDD-Based Symbolic Model Checking
• Propositional SAT Solving
• SAT-Based Model Checking
• Satisfiability Modulo Theories
• Compositional Reasoning
• Abstraction and Abstraction Refinement
• Interpolation and Model Checking
• Predicate Abstraction for Program Verification
• Combining Model Checking and Data-Flow Analysis
• Model Checking Procedural Programs
• Model Checking Concurrent Programs
• Combining Model Checking and Testing
• Combining Model Checking and Deduction
• Model Checking Parameterized Systems
• Model Checking Security Protocols
• Transfer of Model Checking to Industrial Practice
• Functional Specification of Hardware via Temporal Logic
• Symbolic Trajectory Evaluation
• The mu-calculus and Model Checking
• Graph Games and Reactive Synthesis
• Model Checking Probabilistic Systems
• Model Checking Real-Time Systems
• Verification of Hybrid Systems
• Symbolic Model Checking in Non-Boolean Domains
• Process Algebra and Model Checking.