Systems and Software Verification
Model-Checking Techniques and Tools
Authors: Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.
Free PreviewBuy this book
- About this book
-
Model checking is a powerful approach for the formal verification of software. When applicable, it automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct.
This book provides a basic introduction to this new technique. The first part describes in simple terms the theoretical basis of model checking: transition systems as a formal model of systems, temporal logic as a formal language for behavioral properties, and model-checking algorithms. The second part explains how to write rich and structured temporal logic specifications in practice, while the third part surveys some of the major model checkers available.
- Table of contents (17 chapters)
-
-
Automata
Pages 5-26
-
Temporal Logic
Pages 27-38
-
Model Checking
Pages 39-46
-
Symbolic Model Checking
Pages 47-58
-
Timed Automata
Pages 59-72
-
Table of contents (17 chapters)
Recommended for you
Bibliographic Information
- Bibliographic Information
-
- Book Title
- Systems and Software Verification
- Book Subtitle
- Model-Checking Techniques and Tools
- Authors
-
- B. Berard
- M. Bidoit
- A. Finkel
- F. Laroussinie
- A. Petit
- L. Petrucci
- P. Schnoebelen
- Translated by
- McKenzie, P.
- Copyright
- 2001
- Publisher
- Springer-Verlag Berlin Heidelberg
- Copyright Holder
- Springer-Verlag Berlin Heidelberg
- eBook ISBN
- 978-3-662-04558-9
- DOI
- 10.1007/978-3-662-04558-9
- Hardcover ISBN
- 978-3-540-41523-7
- Softcover ISBN
- 978-3-642-07478-3
- Edition Number
- 1
- Number of Pages
- XII, 190
- Additional Information
- Original French edition published by Vuibert, Paris, 1999
- Topics
