Skip to main content
  • Book
  • © 2001

Systems and Software Verification

Model-Checking Techniques and Tools

  • An introduction to software verification
  • Includes supplementary material: sn.pub/extras

Buy it now

Buying options

eBook USD 119.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 159.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 159.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (17 chapters)

  1. Front Matter

    Pages I-XII
  2. Principles and Techniques

    1. Front Matter

      Pages 1-3
    2. Automata

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 5-26
    3. Temporal Logic

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 27-38
    4. Model Checking

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 39-46
    5. Symbolic Model Checking

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 47-58
    6. Timed Automata

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 59-72
  3. Specifying with Temporal Logic

    1. Front Matter

      Pages 75-78
    2. Reachability Properties

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 79-81
    3. Safety Properties

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 83-89
    4. Liveness Properties

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 91-98
    5. Deadlock-freeness

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 99-101
    6. Fairness Properties

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 103-107
    7. Abstraction Methods

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 109-123
  4. Some Tools

    1. Front Matter

      Pages 127-130
    2. SMV — Symbolic Model Checking

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 131-138
    3. SPIN — Communicating Automata

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 139-144
    4. DESIGN/CPN — Coloured Petri Nets

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 145-151
    5. UPPAAL — Timed Systems

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 153-159
    6. KRONOS — Model Checking of Real-time Systems

      • Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci et al.
      Pages 161-168

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.

Authors and Affiliations

  • Laboratoire Spécification et Vérification, CNRS, UMR 8643, Ecole Normale Supérieure de Cachan, Cachan Cedex, France

    Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen

  • Département d’Informatique et Recherche Opérationnelle, Université de Montréal, Montréal, Canada

    Pierre McKenzie

Bibliographic Information

Buy it now

Buying options

eBook USD 119.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 159.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 159.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access