Systems and software verification

Nowadays, validation and verification of computer systems and algorithms are key ingredients in the design and development of high-tech applications. Mastering them is crucial for industrial and economical success.
Different techniques exist for the formal verification of critical systems (or part of them).This book is dedicated to model checking, one of the most widespread and efficient of these techniques.
Model checkers are used routinely by system designers to discover design errors at an earlier stage in the project.They are quickly becoming part of the standard toolkit, especially in application domains such as:
-communication protocols
-VLSI circuits
-programmable logic controllers
-telephone services.
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, symbolic model checking,timed systems).The second part focuses on the practical problem of writing correctness properties in temporal logic, and on different approaches to their verification.The third part reviews several model-checking tools.
The main authors are professors or researchers at the Laboratoire Spécification et Vérifkation (LSV), a joint laboratory of École Normale Supérieure de Cachan and Centre National de la Recherche Scientifique (France).The LSV is a leading team in formal verification and related domains (see http://www.isv.ens-cachan.fr).

Contents

• Principles and techniques
• Specifying with temporal logic
• Some tools
• Main bibliography
• Index