constant (which more generally implies the tractability of model checking for monadic second-order logic), bounding the degree of every domain element, and more general conditions such as bounded expansion, locally bounded expansion, and nowhere-dense structures. These results have been extended to the task of enumerating all solutions to a first-order formula with free variables. Tools Here is a list of significant model-checking tools: Alloy (Alloy Analyzer) BLAST (Berkeley Lazy Abstraction Software Verification Tool) CADP (Construction and Analysis of Distributed Processes) a toolbox for the design of communication protocols and distributed systems CPAchecker: an open-source software model checker for C programs, based on the CPA framework ECLAIR: a platform for the automatic analysis, verification, testing, and transformation of C and C++ programs FDR2: a model checker for verifying real-time systems modelled and specified as CSP Processes ISP code level verifier for MPI programs Java Pathfinder: an open-source model checker for Java programs Libdmc: a framework for distributed model checking mCRL2 Toolset, Boost Software License, Based on ACP NuSMV: a new symbolic model checker PAT: an enhanced simulator, model checker and refinement checker for concurrent and real-time systems Prism: a probabilistic symbolic model checker Roméo: an integrated tool environment for modelling, simulation, and verification of real-time systems modelled as parametric, time, and stopwatch Petri nets SPIN: a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion Storm: A model checker for probabilistic systems. TAPAs: a tool for the analysis of process algebra TAPAAL: an integrated tool environment for modelling, validation, and verification of Timed-Arc Petri Nets TLA+ model checker by Leslie Lamport UPPAAL: an integrated tool environment for modelling, validation, and verification of real-time systems modelled as networks of timed automata Zing – experimental tool from Microsoft to validate state models of software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system. Zing is currently being used for developing drivers for Windows. See also References Further reading . JA Bergstra, A. Ponse and SA Smolka, editors." (). (this is also a very good introduction and overview of model checking)