Normal view MARC view ISBD view

Model checking / Edmund M. Clarke, Jr. ... [et al.].

Contributor(s): Clarke, Edmund M., Jr. (Edmund Melson), 1945-.
Material type: materialTypeLabelBookCall no.: QA76.76.V47 M63 2018Series: Cyber-physical systems series: Publication: Cambridge, Massachusetts : The MIT Press, c2018Edition: 2nd ed.Description: xx, 402 p. : ill.ISBN: 9780262038836; 0262038838.Subject(s): Computer systems -- Verification
Contents:
1.Introduction to the second edition -- 2.1.The Need for Formal Methods -- 2.2.Hardware and Software Verification -- 2.3.The Process of Model Checking -- 2.4.Temporal Logic and Model Checking -- 2.5.Symbolic Algorithms -- 2.6.Partial Order Reduction -- 2.7.Other Approaches to the State Explosion Problem -- 3.1.Transition Systems and Kripke Structures -- 3.2.Nondeterminism and Inputs -- 3.3.First-Order Logic and Symbolic Representations -- 3.4.Boolean Encoding -- 3.5.Modeling Digital Circuits -- 3.6.Modeling Programs -- 3.7.Fairness -- 4.1.The Computation Tree Logic CTL* -- 4.2.Syntax and Semantics of CTL* -- 4.3.Temporal Logics Based on CTL* -- 4.4.Temporal Logic with Set Atomic Propositions and Set Semantics -- 4.5.Fairness -- 4.6.Counterexamples -- 4.7.Safety and Liveness Properties -- 5.1.Explicit-State CTL Model Checking -- 5.2.Model-Checking CTL with Fairness Constraints -- 5.3.CTL Model Checking via Fixpoint Computation -- 6.1.The Tableau Construction
6.2.LTL Model Checking with Tableau -- 6.3.Correctness Proof of the Tableau Construction -- 6.4.CTL* Model Checking -- 7.1.Finite Automata on Finite Words -- 7.2.Automata on Infinite Words -- 7.3.Deterministic versus Nondeterministic Buchi Automata -- 7.4.Intersection of Buchi Automata -- 7.5.Checking Emptiness -- 7.6.Generalized Buchi Automata -- 7.7.Automata and Kripke Structures -- 7.8.Model Checking using Automata -- 7.9.From LTL to Buchi Automata -- 7.10.Efficient Translation of LTL into Automata -- 7.11.On-the-Fly Model Checking -- 8.1.Representing Boolean Formulas -- 8.2.Representing Kripke Structures with OBDDs -- 8.3.Symbolic Model Checking for CTL -- 8.4.Fairness in Symbolic Model Checking -- 8.5.Counterexamples and Witnesses -- 8.6.Relational Product Computations -- 9.1.Conjunctive Normal Form -- 9.2.Encoding Propositional Logic into CNF -- 9.3.Propositional Satisfiability using Binary Search -- 9.4.Boolean Constraint Propagation (BCP)
9.5.Conflict-Driven Clause Learning -- 9.6.Decision Heuristics -- 10.1.Bounded Model Checking -- 10.2.Verifying Reachability Properties with k-Induction -- 10.3.Model Checking with Inductive Invariants -- 10.4.Model Checking with Craig Interpolants -- 10.5.Property-Directed Reachability -- 11.1.Bisimulation Equivalence -- 11.2.Fair Bisimulation -- 11.3.Preorders between Structures -- 11.4.Games for Bisimulation and Simulation -- 11.5.Equivalence and Preorder Algorithms -- 12.1.Concurrency in Asynchronous Systems -- 12.2.Independence and Invisibility -- 12.3.Partial Order Reduction for LTL_x -- 12.4.An Example -- 12.5.Calculating Ample Sets -- 12.6.Correctness of the Algorithm -- 12.7.Partial Order Reduction in SPIN -- 13.1.Existential Abstraction -- 13.2.Computation of Abstract Models -- 13.3.Counterexample-Guided Abstraction Refinement (CEGAR) -- 14.1.Representing Programs as Control-Flow Graphs -- 14.2.Checking Assertions using Symbolic Execution
19.4.Quantitative Temporal Analysis: Minimum/Maximum Delay -- 19.5.Example: An Aircraft Controller -- 20.1.Timed Automata -- 20.2.Parallel Composition -- 20.3.Modeling with Timed Automata -- 20.4.Clock Regions -- 20.5.Clock Zones -- 20.6.Difference-Bound Matrices -- 20.7.Complexity Considerations.
Summary: "An expanded and updated edition of a comprehensive presentation of the theory and practice of model checking, a technology that automates the analysis of complex systems"
Tags from this library: No tags from this library for this title. Log in to add tags.
    average rating: 0.0 (0 votes)
Item type Current location Collection Call number Status Date due Barcode Item holds
Book Book Boonchoo Treethong Library, Lampang Campus
General Stacks
General Books QA76.76.V47 M63 2018 (See Similar Items) Available 31379015679641
Book Book Puey Ungphakorn Library, Rangsit Campus
General Stacks
General Books QA76.76.V47 M63 2018 (See Similar Items) Show map Available 31379015740419
Total holds: 0

Includes bibliographical references (pages [367]-397) and index.

1.Introduction to the second edition -- 2.1.The Need for Formal Methods -- 2.2.Hardware and Software Verification -- 2.3.The Process of Model Checking -- 2.4.Temporal Logic and Model Checking -- 2.5.Symbolic Algorithms -- 2.6.Partial Order Reduction -- 2.7.Other Approaches to the State Explosion Problem -- 3.1.Transition Systems and Kripke Structures -- 3.2.Nondeterminism and Inputs -- 3.3.First-Order Logic and Symbolic Representations -- 3.4.Boolean Encoding -- 3.5.Modeling Digital Circuits -- 3.6.Modeling Programs -- 3.7.Fairness -- 4.1.The Computation Tree Logic CTL* -- 4.2.Syntax and Semantics of CTL* -- 4.3.Temporal Logics Based on CTL* -- 4.4.Temporal Logic with Set Atomic Propositions and Set Semantics -- 4.5.Fairness -- 4.6.Counterexamples -- 4.7.Safety and Liveness Properties -- 5.1.Explicit-State CTL Model Checking -- 5.2.Model-Checking CTL with Fairness Constraints -- 5.3.CTL Model Checking via Fixpoint Computation -- 6.1.The Tableau Construction

6.2.LTL Model Checking with Tableau -- 6.3.Correctness Proof of the Tableau Construction -- 6.4.CTL* Model Checking -- 7.1.Finite Automata on Finite Words -- 7.2.Automata on Infinite Words -- 7.3.Deterministic versus Nondeterministic Buchi Automata -- 7.4.Intersection of Buchi Automata -- 7.5.Checking Emptiness -- 7.6.Generalized Buchi Automata -- 7.7.Automata and Kripke Structures -- 7.8.Model Checking using Automata -- 7.9.From LTL to Buchi Automata -- 7.10.Efficient Translation of LTL into Automata -- 7.11.On-the-Fly Model Checking -- 8.1.Representing Boolean Formulas -- 8.2.Representing Kripke Structures with OBDDs -- 8.3.Symbolic Model Checking for CTL -- 8.4.Fairness in Symbolic Model Checking -- 8.5.Counterexamples and Witnesses -- 8.6.Relational Product Computations -- 9.1.Conjunctive Normal Form -- 9.2.Encoding Propositional Logic into CNF -- 9.3.Propositional Satisfiability using Binary Search -- 9.4.Boolean Constraint Propagation (BCP)

9.5.Conflict-Driven Clause Learning -- 9.6.Decision Heuristics -- 10.1.Bounded Model Checking -- 10.2.Verifying Reachability Properties with k-Induction -- 10.3.Model Checking with Inductive Invariants -- 10.4.Model Checking with Craig Interpolants -- 10.5.Property-Directed Reachability -- 11.1.Bisimulation Equivalence -- 11.2.Fair Bisimulation -- 11.3.Preorders between Structures -- 11.4.Games for Bisimulation and Simulation -- 11.5.Equivalence and Preorder Algorithms -- 12.1.Concurrency in Asynchronous Systems -- 12.2.Independence and Invisibility -- 12.3.Partial Order Reduction for LTL_x -- 12.4.An Example -- 12.5.Calculating Ample Sets -- 12.6.Correctness of the Algorithm -- 12.7.Partial Order Reduction in SPIN -- 13.1.Existential Abstraction -- 13.2.Computation of Abstract Models -- 13.3.Counterexample-Guided Abstraction Refinement (CEGAR) -- 14.1.Representing Programs as Control-Flow Graphs -- 14.2.Checking Assertions using Symbolic Execution

19.4.Quantitative Temporal Analysis: Minimum/Maximum Delay -- 19.5.Example: An Aircraft Controller -- 20.1.Timed Automata -- 20.2.Parallel Composition -- 20.3.Modeling with Timed Automata -- 20.4.Clock Regions -- 20.5.Clock Zones -- 20.6.Difference-Bound Matrices -- 20.7.Complexity Considerations.

"An expanded and updated edition of a comprehensive presentation of the theory and practice of model checking, a technology that automates the analysis of complex systems"

There are no comments for this item.

Click on an image to view it in the image viewer

Open Library:

Thammasat University Library
2 Prachan Road, Phranakorn, Bangkok 10200
Tel: 662 613-3544 (Pridi Banomyong Library, Circulation Desk)
Tel: 662 564-4444 ext. 1305 (Puey Ungphakorn Library (Rangsit Campus), Circulation Desk)