Systems and Software Verification: Model-Checking Techniques and Tools by B. BerardSystems and Software Verification: Model-Checking Techniques and Tools by B. Berard

Systems and Software Verification: Model-Checking Techniques and Tools

byB. Berard, P. McKenzie, A. Finkel

Paperback | December 15, 2010

Pricing and Purchase Info

$143.83 online 
$164.50 list price save 12%
Earn 719 plum® points

Prices and offers may vary in store


In stock online

Ships free on orders over $25

Not available in stores


Model checking is a powerful approach for the formal verification of software. It automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct. Here, the author provides a well written and basic introduction to the 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.
Title:Systems and Software Verification: Model-Checking Techniques and ToolsFormat:PaperbackDimensions:190 pagesPublished:December 15, 2010Publisher:Springer-Verlag/Sci-Tech/TradeLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:3642074782

ISBN - 13:9783642074783

Look for similar items by category:


Table of Contents

Part I: Principles and Techniques: Introduction; 1. Automata; 2. Temporal Logic; 3. Model Checking; 4. Symbolic Model Checking; 5. Timed Automata; Conclusion. Part II: Specifying with Temporal Logic: Introduction; 6. Reachability Properties; 7. Safety Properties; 8. Liveness Properties; 9. Deadlock-freeness; 10. Fairness Properties; 11. Abstraction Methods; Conclusion. Part III: Some Tools: Introduction; 12. SMV - Symbolic Model Checking; 13. Spin - Communication Automata; 14. Design/CPN - Coloured Petri Nets; 15. Uppaal - Timed Systems; 16. Kronos - Model Checking of Real-time Systems; 17. HyTech - Linear Hybrid Systems; Main Bibliography; Index.