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…
"This book is the first text on model checking at a graduate/undergraduate level. It is divided into three parts. The first part is concerned with the fundamental notions (modelling with finite automata, synchronous product of automata, temporal logic, model-checking algorithms,…
The focus of this book is on bridging the gap between two extreme methods for developing software. On the one hand, there are texts and approaches that are so formal that they scare off all but the most dedicated theoretical computer scientists. On the other, there are some who …
This textbook on program verification emphasises the role of verification in software development.
