Clarke, E. M., 1945-
Model checking / Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. - Cambridge, Mass. : MIT Press, c1999. - xiv, 314 p. ; 24 cm.
Foreword by Amir Pnueli. - Preface. - 1. Introduction. - 2. Modeling Systems. - 3. Temporal Logics. - 4. Model Checking. - 5. Binary Decision Diagram. - 6. Symbolic Model Checking. - 7. Model Checking for the [mu]-Calculus. - 8. Model Checking in Practice. - 9. Model Checking and Automata Theory. - 10. Partial Order Reduction. - 11. Equivalences and Preorders between Structures. - 12. Compositional Reasoning. - 13. Abstraction. - 14. Symmetry. - 15. Infinite Families of Finite-State Systems. - 16. Discrete Real-Time and Quantitative Temporal Analysis. - 17. Continuous Real Time. - 18. Conclusion. - References. - Index.
"This book is the first comprehensive presentation of the theory and practice of model checking. The book, which includes basic as well as state-of-the-art techniques, algorithms, and tools, can be used both as an intoduction to the subject and as a reference for reserachers." - Front cover
0262032708
Computer systems--Verification.
004.21 / CLA
Model checking / Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. - Cambridge, Mass. : MIT Press, c1999. - xiv, 314 p. ; 24 cm.
Foreword by Amir Pnueli. - Preface. - 1. Introduction. - 2. Modeling Systems. - 3. Temporal Logics. - 4. Model Checking. - 5. Binary Decision Diagram. - 6. Symbolic Model Checking. - 7. Model Checking for the [mu]-Calculus. - 8. Model Checking in Practice. - 9. Model Checking and Automata Theory. - 10. Partial Order Reduction. - 11. Equivalences and Preorders between Structures. - 12. Compositional Reasoning. - 13. Abstraction. - 14. Symmetry. - 15. Infinite Families of Finite-State Systems. - 16. Discrete Real-Time and Quantitative Temporal Analysis. - 17. Continuous Real Time. - 18. Conclusion. - References. - Index.
"This book is the first comprehensive presentation of the theory and practice of model checking. The book, which includes basic as well as state-of-the-art techniques, algorithms, and tools, can be used both as an intoduction to the subject and as a reference for reserachers." - Front cover
0262032708
Computer systems--Verification.
004.21 / CLA