.1 200 OK date: Thu, 02 Jul 2026 13:03:24 GMT server: mw-web.codfw.main-59656c8c96-56ww8 x-content-type-options: nosniff content-language: en accept-ch: reporting-endpoints: csp-report-to-endpoint='/w/api.php?action=cspreport&format=json'; content-security-policy: script-src 'unsafe-eval' blob: 'self' meta.wikimedia.org *.wikimedia.org *.wikipedia.org *.wikinews.org *.wiktionary.org *.wikibooks.org *.wikiversity.org *.wikisource.org wikisource.org *.wikiquote.org *.wikidata.org *.wikifunctions.org *.wikivoyage.org *.mediawiki.org mediawiki.org wikimedia.org *.wmflabs.org *.wmcloud.org *.toolforge.org wss://*.toolforge.org *.jsdelivr.net unpkg.com cdnjs.cloudflare.com raw.githubusercontent.com *.github.com code.jquery.com cdn.mathjax.org use.typekit.net fonts.cdnfonts.com use.fontawesome.com i.ytimg.com rsms.me doi.org localhost https://localhost:* http://localhost:* wss://localhost:* ws://localhost:* *.google.com *.gstatic.com *.googleapis.com *.translate.yandex.net yastatic.net ya.ru radically.github.io cdn.sammdot.ca cdn.fontshare.com viaf.org publicai-proxy.alaexis.workers.dev iiif.archive.org api.flickr.com live.staticflickr.com api.anthropic.com api.openai.com api.publicai.co catalogo.pusc.it parsifal.urbe.it opac.sbn.it overpass-api.de api.openrouteservice.org archive.org *.openstreetmap.org *.waymarkedtrails.org *.thunderforest.com registry.ipe.wiki analytics.ipe.wiki qlever.dev app.goacoustic.com wikipedia-archive.ourworldindata.org api.inaturalist.org inaturalist-open-data.s3.amazonaws.com validator.w3.org db.onlinewebfonts.com fontlibrary.org 'unsafe-inline' auth.wikimedia.org; default-src 'self' data: blob: upload.wikimedia.org https://commons.wikimedia.org meta.wikimedia.org *.wikimedia.org *.wikipedia.org *.wikinews.org *.wiktionary.org *.wikibooks.org *.wikiversity.org *.wikisource.org wikisource.org *.wikiquote.org *.wikidata.org *.wikifunctions.org *.wikivoyage.org *.mediawiki.org mediawiki.org wikimedia.org *.wmflabs.org *.wmcloud.org *.toolforge.org wss://*.toolforge.org *.jsdelivr.net unpkg.com cdnjs.cloudflare.com raw.githubusercontent.com *.github.com code.jquery.com cdn.mathjax.org use.typekit.net fonts.cdnfonts.com use.fontawesome.com i.ytimg.com rsms.me doi.org localhost https://localhost:* http://localhost:* wss://localhost:* ws://localhost:* *.google.com *.gstatic.com *.googleapis.com *.translate.yandex.net yastatic.net ya.ru radically.github.io cdn.sammdot.ca cdn.fontshare.com viaf.org publicai-proxy.alaexis.workers.dev iiif.archive.org api.flickr.com live.staticflickr.com api.anthropic.com api.openai.com api.publicai.co catalogo.pusc.it parsifal.urbe.it opac.sbn.it overpass-api.de api.openrouteservice.org archive.org *.openstreetmap.org *.waymarkedtrails.org *.thunderforest.com registry.ipe.wiki analytics.ipe.wiki qlever.dev app.goacoustic.com wikipedia-archive.ourworldindata.org api.inaturalist.org inaturalist-open-data.s3.amazonaws.com validator.w3.org db.onlinewebfonts.com fontlibrary.org en.wikibooks.org en.wikinews.org en.wikiquote.org en.wikisource.org en.wikiversity.org en.wikivoyage.org en.wiktionary.org www.mediawiki.org commons.wikimedia.org foundation.wikimedia.org incubator.wikimedia.org species.wikimedia.org wikimania.wikimedia.org www.wikidata.org www.wikifunctions.org auth.wikimedia.org; style-src 'self' data: blob: upload.wikimedia.org https://commons.wikimedia.org meta.wikimedia.org *.wikimedia.org *.wikipedia.org *.wikinews.org *.wiktionary.org *.wikibooks.org *.wikiversity.org *.wikisource.org wikisource.org *.wikiquote.org *.wikidata.org *.wikifunctions.org *.wikivoyage.org *.mediawiki.org mediawiki.org wikimedia.org *.wmflabs.org *.wmcloud.org *.toolforge.org wss://*.toolforge.org *.jsdelivr.net unpkg.com cdnjs.cloudflare.com raw.githubusercontent.com *.github.com code.jquery.com cdn.mathjax.org use.typekit.net fonts.cdnfonts.com use.fontawesome.com i.ytimg.com rsms.me doi.org localhost https://localhost:* http://localhost:* wss://localhost:* ws://localhost:* *.google.com *.gstatic.com *.googleapis.com *.translate.yandex.net yastatic.net ya.ru radically.github.io cdn.sammdot.ca cdn.fontshare.com viaf.org publicai-proxy.alaexis.workers.dev iiif.archive.org api.flickr.com live.staticflickr.com api.anthropic.com api.openai.com api.publicai.co catalogo.pusc.it parsifal.urbe.it opac.sbn.it overpass-api.de api.openrouteservice.org archive.org *.openstreetmap.org *.waymarkedtrails.org *.thunderforest.com registry.ipe.wiki analytics.ipe.wiki qlever.dev app.goacoustic.com wikipedia-archive.ourworldindata.org api.inaturalist.org inaturalist-open-data.s3.amazonaws.com validator.w3.org db.onlinewebfonts.com fontlibrary.org 'unsafe-inline'; object-src 'none'; report-uri /w/api.php?action=cspreport&format=json; report-to csp-report-to-endpoint last-modified: Thu, 18 Jun 2026 13:03:24 GMT content-type: text/html; charset=UTF-8 age: 0 accept-ranges: bytes x-cache: cp2047 miss, cp2047 miss x-cache-status: miss server-timing: cache;desc="miss", host;desc="cp2047" strict-transport-security: max-age=106384710; includeSubDomains; preload report-to: { "group": "wm_nel", "max_age": 604800, "endpoints": [{ "url": "https://intake-logging.wikimedia.org/v1/events?stream=w3c.reportingapi.network_error&schema_uri=/w3c/reportingapi/network_error/1.0.0" }] } nel: { "report_to": "wm_nel", "max_age": 604800, "failure_fraction": 0.05, "success_fraction": 0.0} set-cookie: WMF-Last-Access=02-Jul-2026;Path=/;HttpOnly;secure;Expires=Mon, 03 Aug 2026 12:00:00 GMT set-cookie: WMF-Last-Access-Global=02-Jul-2026;Path=/;Domain=.wikipedia.org;HttpOnly;secure;Expires=Mon, 03 Aug 2026 12:00:00 GMT set-cookie: WMF-DP=18f;Path=/;HttpOnly;secure;Expires=Fri, 03 Jul 2026 00:00:00 GMT x-client-ip: 75.28.18.94 cache-control: private, s-maxage=0, max-age=0, must-revalidate, no-transform vary: Accept-Encoding,X-Subdomain,Cookie,Authorization,User-Agent set-cookie: GeoIP=US:TX:McKinney:33.20:-96.62:v4; Path=/; secure; Domain=.wikipedia.org set-cookie: NetworkProbeLimit=0.001;Path=/;Secure;SameSite=None;Max-Age=3600 set-cookie: WMF-Uniq=kkUsHQ8twVr9QZch1zSLjwORAAAAAFvdtQCZ5gMhHBmGhvFl7XBDtPUfK3r83qwL;Domain=.wikipedia.org;Path=/;HttpOnly;secure;SameSite=None;Expires=Fri, 02 Jul 2027 00:00:00 GMT transfer-encoding: chunked x-request-id: a762272b-4688-44fd-9ee3-e56dbb92cb10 x-analytics: 8000 Model checking - Wikipedia Jump to content Main menu Main menu move to sidebar hide Navigation Main page Contents Current events Random article About Wikipedia Contact us Contribute Help Learn to edit Community portal Recent changes Upload file Special pages Search Search Appearance Donate Create account Log in Personal tools Donate Create account Log in Contents move to sidebar hide (Top) 1 Overview 2 Symbolic model checking Toggle Symbolic model checking subsection 2.1 Example 3 Techniques 4 First-order logic 5 Tools 6 See also 7 References 8 Further reading Toggle the table of contents Model checking 15 languages Català Deutsch Ελληνικά Español فارسی Français Italiano 日本語 Português Русский Slovenčina Türkçe Украї 8000 нська Tiếng Việt 中文 Edit links Article Talk English Read Edit View history Tools Tools move to sidebar hide Actions Read Edit View history General What links here Related changes Upload file Permanent link Page information Cite this page Get shortened URL Switch to legacy parser Print/export Download as PDF Printable version In other projects Wikimedia Commons Wikidata item Appearance move to sidebar hide From Wikipedia, the free encyclopedia Computer science field This article is about checking of models in computer science. For the checking of models in statistics, see statistical model validation . Elevator control software can be model-checked to verify both safety properties, like "The cabin never moves with its door open" , [ 1 ] and liveness properties, like "Whenever the n th floor's call button is pressed, the cabin will eventually stop at the n th floor and open the door" . In computer science , model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness ). This is typically associated with hardware or software systems , where the specification contains liveness requirements (such as avoidance of livelock ) as well as safety requirements (such as avoidance of states representing a system crash ). In order to solve such a problem algorithmically , both the model of the system and its specification are formulated in some precise mathematical language. To this end, the problem is formulated as a task in logic , namely to check whether a structure satisfies a given logical formula. This general concept applies to many kinds of logic and many kinds of structures. A simple model-checking problem consists of verifying whether a formula in the propositional logic is satisfied by a given structure. Overview [ edit ] Property checking is used for verification when two descriptions are not equivalent. During refinement , the specification is complemented with details that are unnecessary in the higher-level specification. There is no need to verify the newly introduced properties against the original specification since this is not possible. Therefore, the strict bi-directional equivalence check is relaxed to a one-way property check. The implementation or design is regarded as a model of the system, whereas the specifications are properties that the model must satisfy. [ 2 ] An important class of model-checking methods has been developed for checking models of hardware and software designs where the specification is given by a temporal logic formula. Pioneering work in temporal logic specification was done by Amir Pnueli , who received the 1996 Turing award for "seminal work introducing temporal logic into computing science". [ 3 ] Model checking began with the pioneering work of E. M. Clarke , E. A. Emerson , [ 4 ] [ 5 ] [ 6 ] by J. P. Queille, and J. Sifakis . [ 7 ] Clarke, Emerson, and Sifakis shared the 2007 Turing Award for their seminal work founding and developing the field of model checking. [ 8 ] [ 9 ] Model checking is most often applied to hardware designs. For software, because of undecidability (see computability theory ) the approach cannot be fully algorithmic, apply to all systems, and always give an answer; in the general case, it may fail to prove or disprove a given property. In embedded-systems hardware, it is possible to validate a specification delivered, e.g., by means of UML activity diagrams [ 10 ] or control-interpreted Petri nets . [ 11 ] The structure is usually given as a source code description in an industrial hardware description language or a special-purpose language. Such a program corresponds to a finite-state machine (FSM), i.e., a directed graph consisting of nodes (or vertices ) and edges . A set of atomic propositions is associated with each node, typically stating which memory elements are one. The nodes represent states of a system, the edges represent possible transitions that may alter the state, while the atomic propositions represent the basic properties that hold at a point of execution. [ 12 ] Formally, the problem can be stated as follows: given a desired property, expressed as a temporal logic formula p {\displaystyle p} , and a structure M {\displaystyle M} with initial state s {\displaystyle s} , decide if M , s ⊨ p {\displaystyle M,s\models p} . If M {\displaystyle M} is finite, as it is in hardware, model checking reduces to a graph search . Symbolic model checking [ edit ] Instead of enumerating reachable states one at a time, the state space can sometimes be traversed more efficiently by considering large numbers of states at a single step. When such state-space traversal is based on representations of a set of states and transition relations as logical formulas, binary decision diagrams (BDD) or other related data structures, the model-checking method is symbolic . Historically, the first symbolic methods used BDDs . After the success of propositional satisfiability in solving the planning problem in artificial intelligence (see satplan ) in 1996, the same approach was generalized to model checking for linear temporal logic (LTL): the planning problem corresponds to model checking for safety properties. This method is known as bounded model checking. [ 13 ] The success of Boolean satisfiability solvers in bounded model checking led to the widespread use of satisfiability solvers in symbolic model checking. [ 14 ] Example [ edit ] One example of such a system requirement: Between the time an elevator is called at a floor and the time it opens its doors at that floor, the elevator can arrive at that floor at most twice . The authors of "Patterns in Property Specification for Finite-State Verification" translate this requirement into the following LTL formula: [ 15 ] ◻ ( ( call ∧ ◊ open ) → ( ( ¬ atfloor ∧ ¬ open ) U ( open ∨ ( ( atfloor ∧ ¬ open ) U ( open ∨ ( ( ¬ atfloor ∧ ¬ open ) U ( open ∨ ( ( atfloor ∧ ¬ open ) U ( open ∨ ( ¬ atfloor U open ) ) ) ) ) ) ) ) ) ) {\displaystyle {\begin{aligned}\Box {\Big (}({\texttt {call}}\land \Diamond {\texttt {open}})\to &{\big (}(\lnot {\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor ((\lnot {\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (({\texttt {atfloor}}\land \lnot {\texttt {open}})~{\mathcal {U}}\\&({\texttt {open}}\lor (\lnot {\texttt {atfloor}}~{\mathcal {U}}~{\texttt {open}})))))))){\big )}{\Big )}\end{aligned}}} Here, ◻ {\displaystyle \Box } should be read as "always", ◊ {\displaystyle \Diamond } as "eventually", U {\displaystyle {\mathcal {U}}} as "until" and the other symbols are standard logical symbols, ∨ {\displaystyle \lor } for "or", ∧ {\displaystyle \land } for "and" and ¬ {\displaystyle \lnot } for "not". Techniques [ edit ] Model-checking tools face a combinatorial blow up of the state-space, commonly known as the state explosion problem , that must be addressed to solve most real-world problems. There are several approaches to combat this problem. Symbolic algorithms avoid ever explicitly constructing the graph for the FSM; instead, they represent the graph implicitly using a formula in quantified propositional logic. The use of binary decision diagrams (BDDs) was made popular by the work of Ken McMillan, [ 16 ] as well as of Olivier Coudert and Jean-Christophe Madre, [ 17 ] and the development of open-source BDD manipulation libraries such as CUDD [ 18 ] and BuDDy. [ 19 ] Bounded model-checking algorithms unroll the FSM for a fixed number of steps, k {\displaystyle k} , and check whether a property violation can occur in k {\displaystyle k} or fewer steps. This typically involves encoding the restricted model as an instance of SAT . The process can be repeated with larger and larger values of k {\displaystyle k} until all possible violations have been ruled out (cf. Iterative deepening depth-first search ). Abstraction attempts to prove properties of a system by first simplifying it. The simplified system usually does not satisfy exactly the same properties as the original one so that a process of refinement may be necessary. Generally, one requires the abstraction to be sound (the properties proved on the abstraction are true of the original system); however, sometimes the abstraction is not complete (not all true properties of the original system are true of the abstraction). An example of abstraction is to ignore the values of non-Boolean variables and to only consider Boolean variables and the control flow of the program; such an abstraction, though it may appear coarse, may, in fact, be sufficient to prove e.g. properties of mutual exclusion . Counterexample-guided abstraction refinement (CEGAR) begins checking with a coarse (i.e. imprecise) abstraction and iteratively refines it. When a violation (i.e. counterexample ) is found, the tool analyzes it for feasibility (i.e., is the violation genuine or the result of an incomplete abstraction?). If the violation is feasible, it is reported to the user. If it is not, the proof of infeasibility is used to refine the abstraction and checking begins again. [ 20 ] Model-checking tools were initially developed to reason about the logical correctness of discrete state systems, but have since been extended to deal with real-time and limited forms of hybrid systems . First-order logic [ edit ] Model checking is also studied in the field of computational complexity theory . Specifically, a first-order logical formula is fixed without free variables and the following decision problem is considered: Given a finite interpretation , for instance, one described as a relational database , decide whether the interpretation is a model of the formula. This problem is in the circuit class AC 0 . It is tractable when imposing some restrictions on the input structure: for instance, requiring that it has treewidth bounded by a 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. [ 21 ] These results have been extended to the task of enumerating all solutions to a first-order formula with free variables. [ citation needed ] Tools [ edit ] Main article: List of model checking tools Here is a list of significant model-checking tools: Afra: a model checker for Rebeca which is an actor-based language for modeling concurrent and reactive systems 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 FizzBee : an easier to use alternative to TLA+, that uses Python-like specification language, that has both behavioral modeling like TLA+ and probabilistic modeling like PRISM 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 : [ 22 ] 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 [ 23 ] – 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 [ edit ] Abstract interpretation Automated theorem proving Binary decision diagram Büchi automaton Computation tree logic Counterexample-guided abstraction refinement Formal verification Linear temporal logic List of model checking tools Partial order reduction Program analysis (computer science) Static code analysis References [ edit ] ↑ For convenience, the example properties are paraphrased in natural language here. Model-checkers require them to be expressed in some formal logic, like LTL . ↑ Lam K., William (2005). "Chapter 1.1: What Is Design Verification?" . Hardware Design Verification: Simulation and Formal Method-Based Approaches . Retrieved December 12, 2012 . ↑ "Amir Pnueli - A.M. Turing Award Laureate" . ↑ Allen Emerson, E.; Clarke, Edmund M. (1980), "Characterizing correctness properties of parallel programs using fixpoints", Automata, Languages and Programming , Lecture Notes in Computer Science, vol. 85, pp. 169– 181, doi : 10.1007/3-540-10003-2_69 , ISBN 978-3-540-10003-4 ↑ Edmund M. Clarke, E. Allen Emerson: "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic" . Logic of Programs 1981: 52-71. ↑ Clarke, E. M.; Emerson, E. A.; Sistla, A. P. (1986), "Automatic verification of finite-state concurrent systems using temporal logic specifications", ACM Transactions on Programming Languages and Systems , 8 (2): 244, doi : 10.1145/5397.5399 , S2CID 52853200 ↑ Queille, J. P.; Sifakis, J. (1982), "Specification and verification of concurrent systems in CESAR", International Symposium on Programming , Lecture Notes in Computer Science, vol. 137, pp. 337– 351, doi : 10.1007/3-540-11494-7_22 , ISBN 978-3-540-11494-9 ↑ "P 8000 ress Release: ACM Turing Award Honors Founders of Automatic Verification Technology" . Archived from the original on 2008-12-28 . Retrieved 2009-01-06 . ↑ USACM : 2007 Turing Award Winners Announced ↑ Grobelna, Iwona; Grobelny, Michał; Adamski, Marian (2014). "Model Checking of UML Activity Diagrams in Logic Controllers Design". Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30 – July 4, 2014, Brunów, Poland . Advances in Intelligent Systems and Computing. Vol. 286. pp. 233– 242. doi : 10.1007/978-3-319-07013-1_22 . ISBN 978-3-319-07012-4 . ↑ I. Grobelna, " Formal verification of embedded logic controller specification with computer deduction in temporal logic ", Przeglad Elektrotechniczny, Vol.87, Issue 12a, pp.47–50, 2011 ↑ This article is based on material taken from Model+checking at the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL , version 1.3 or later. ↑ Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "Bounded Model Checking Using Satisfiability Solving". Formal Methods in System Design . 19 : 7– 34. doi : 10.1023/A:1011276507260 . S2CID 2484208 . ↑ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE . 103 (11): 2021– 2035. doi : 10.1109/JPROC.2015.2455034 . S2CID 10190144 . ↑ Dwyer, M.; Avrunin, G.; Corbett, J. (May 1999). "Patterns in property specifications for finite-state verification". Patterns in Property Specification for Finite-State Verification . Proceedings of the 21st international conference on Software engineering. pp. 411– 420. doi : 10.1145/302405.302672 . ISBN 1581130740 . ↑ Symbolic Model Checking , Kenneth L. McMillan, Kluwer, ISBN 0-7923-9380-5 , also online Archived 2007-06-02 at the Wayback Machine . ↑ Coudert, O.; Madre, J.C. (1990). "A unified framework for the formal verification of sequential circuits" (PDF) . 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers . IEEE Comput. Soc. Press. pp. 126– 129. doi : 10.1109/ICCAD.1990.129859 . ISBN 978-0-8186-2055-3 . ↑ "CUDD: CU Decision Diagram Package" . ↑ "BuDDy – A Binary Decision Diagram Package" . ↑ Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut (2000), "Counterexample-Guided Abstraction Refinement", Computer Aided Verification (PDF) , Lecture Notes in Computer Science, vol. 1855, pp. 154– 169, doi : 10.1007/10722167_15 , ISBN 978-3-540-67770-3 ↑ Dawar, A; Kreutzer, S (2009). "Parameterized complexity of first-order logic" (PDF) . ECCC . S2CID 5856640 . Archived from the original (PDF) on 2019-03-03. ↑ Storm model checker ↑ Zing Further reading [ edit ] Peled, Doron A. ; Pelliccione, Patrizio; Spoletini, Paola (2009). "Model Checking" . Wiley Encyclopedia of Computer Science and Engineering . pp. 1904– 1920. doi : 10.1002/9780470050118.ecse247 . ISBN 978-0-470-05011-8 . S2CID 5371327 . Clarke, Edmund M. ; Grumberg, Orna ; Peled, Doron A. (1999). Model Checking . MIT Press . ISBN 0-262-03270-8 . Berard, B.; Bidoit, M.; Finkel, A.; Laroussinie, F.; Petit, A.; Petrucci, L.; Schnoebelen, P. (20 June 2001). Systems and Software Verification: Model-Checking Techniques and Tools . Springer. ISBN 3-540-41523-8 . Huth, Michael; Ryan, Mark (2004). Logic in Computer Science: Modelling and Reasoning About Systems . Cambridge University Press . Holzmann, Gerard J. The Spin Model Checker: Primer and Reference Manual . Addison-Wesley. ISBN 0-321-22862-6 . Bradfield, Julian; Stirling, Colin (2001). "Modal Logics and mu-Calculi: An Introduction" . Handbook of Process Algebra . Elsevier. pp. 293– 330. doi : 10.1016/B978-044482830-9/50022-9 . ISBN 978-0-444-82830-9 . . JA Bergstra, A. Ponse and SA Smolka, editors." (). "Specification Patterns" . SAnToS Laboratory, Kansas State University. Archived from the original on 2011-07-19. "Property Pattern Mappings for RAFMC" . CADP:Construction and Analysis of Distributed Processes . 2019. Mateescu, Radu; Sighireanu, Mihaela (2003). "Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus" (PDF) . Science of Computer Programming . 46 (3): 255– 281. doi : 10.1016/S0167-6423(02)00094-1 . S2CID 10942856 . Müller-Olm, M.; Schmidt, D.A.; Steffen, B. (1999). "Model checking: a tutorial introduction". Static Analysis: 6th International Symposium, SAS'99, Venice, Italy, September 22-24, 1999, Proceedings . Vol. 1694. LNCS: Springer. pp. 330– 354. CiteSeerX 10.1.1.96.3011 . doi : 10.1007/3-540-48294-6_22 . ISBN 978-3-540-48294-9 . Baier, C. ; Katoen, J. (2008). Principles of Model Checking . MIT Press. ISBN 978-0-262-30403-0 . Clarke, E.M. (2008). "The Birth of Model Checking". 25 Years of Model Checking . Lecture Notes in Computer Science. Vol. 5000. pp. 1– 26. doi : 10.1007/978-3-540-69850-0_1 . ISBN 978-3-540-69849-4 . Emerson, E. Allen (2008). "The Beginning of Model Checking: A Personal Perspective". In Grumberg, Orna; Veith, Helmut (eds.). 25 Years of Model Checking — History, Achievements, Perspectives . LNCS. Vol. 5000. Springer. pp. 27– 45. doi : 10.1007/978-3-540-69850-0_2 . ISBN 978-3-540-69849-4 . (this is also a very good introduction and overview of model checking) v t e Program analysis Key concepts Control-flow graph Correctness Hyperproperties Invariants Path explosion Polyvariance Rice's theorem Runtime verification Safety and liveness Undefined behavior Semantics Types Axiomatic Denotational Categorical semantics Operational Big-step Small-step Models Lambda calculus Petri net Process calculus Rewriting system State machine Turing machine Analyses Static Abstract interpretation Alias Control flow kCFA Data-flow Dependence Effect system Escape Model checking Pointer Shape Symbolic execution Termination Type systems Typestate Dynamic Data-flow Taint tracking Concolic testing Fuzzing Invariant inference Program slicing Testing Formal methods Concepts Curry–Howard correspondence Loop invariant Refinement Side effect Soundness and completeness Specification Languages Verification Logics Hoare Incorrectness Linear Separation Temporal Data structures BDD E-graph Hashcons Union-find Tools Constraint solvers CHC SAT SMT Lightweight Alloy TLA + Proof assistants ACL2 Agda F* HOL Light HOL4 Idris Isabelle Isabelle/HOL Lean LEGO Mizar NuPRL PVS Rocq Twelf Category Outline Glossary Retrieved from " https://en.wikipedia.org/w/index.php?title=Model_checking&oldid=1322864131 " Categories : Model checking Logic in computer science Hidden categories: Articles with short description Short description is different from Wikidata Webarchive template wayback links All articles with unsourced statements Articles with unsourced statements from May 2019 This page was last edited on 18 November 2025, at 08:25  (UTC) . Page was rendered with Parsoid . Text is available under the Creative Commons Attribution-ShareAlike 4.0 License ; additional terms may apply. By using this site, you agree to the Terms of Use and Privacy Policy . Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc. , a non-profit organization. Privacy policy About Wikipedia Disclaimers Contact Wikipedia Legal & safety contacts Code of Conduct Developers Statistics Cookie statement Mobile view Search Search Toggle the table of contents Model checking 15 languages Add topic 0