Handbook of Model Checking, 2 Teile

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.