{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T03:40:07Z","timestamp":1738986007241,"version":"3.37.0"},"edition-number":"1","reference-count":100,"publisher":"Wiley","isbn-type":[{"type":"print","value":"9780471383932"},{"type":"electronic","value":"9780470050118"}],"license":[{"start":{"date-parts":[[2009,3,16]],"date-time":"2009-03-16T00:00:00Z","timestamp":1237161600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/doi.wiley.com\/10.1002\/tdm_license_1.1"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Model checking is an automatic technique for verifying models of software or hardware systems against their specification. This analysis is based on an exploration of the checked system's state space, hence, it is in general affected by the state explosion problem. In this article, we present the classic model checking approaches and different techniques to deal with the complexity problem. We also describe some popular model checking systems.<\/jats:p>","DOI":"10.1002\/9780470050118.ecse247","type":"other","created":{"date-parts":[[2009,3,9]],"date-time":"2009-03-09T17:48:02Z","timestamp":1236620882000},"page":"1904-1920","source":"Crossref","is-referenced-by-count":13,"title":["Model Checking"],"prefix":"10.1002","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[]},{"given":"Patrizio","family":"Pelliccione","sequence":"additional","affiliation":[]},{"given":"Paola","family":"Spoletini","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2009,3,16]]},"reference":[{"volume-title":"Logic of Programs","year":"1982","author":"Clarke E. M.","key":"e_1_2_11_2_1"},{"key":"e_1_2_11_3_1","doi-asserted-by":"crossref","unstructured":"J. P.Queille andJ.Sifakis Specification and verification of concurrent systems in CESAR Proc. of the 5th Colloquium on International Symposium on Programming 1982 pp.337\u2013351.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"e_1_2_11_4_1","unstructured":"E. M.Clarke andJ. M.Wing Formal methods: State of the art and future directions Technical ReportCMU\u2010CS\u201096\u2010178 Carnegie Mellon University 1996."},{"key":"e_1_2_11_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"e_1_2_11_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"e_1_2_11_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/230514.571645"},{"key":"e_1_2_11_8_1","doi-asserted-by":"crossref","unstructured":"A.Groce andW.Visser Heuristic model checking for java programs Proc. of the 9th International SPIN Workshop on Model Checking of Software 2002 pp.242\u2013245.","DOI":"10.1007\/3-540-46017-9_21"},{"key":"e_1_2_11_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050074"},{"key":"e_1_2_11_10_1","doi-asserted-by":"crossref","unstructured":"J.Bormann J.Lohse M.Payer andG.Venzl Model checking in industrial hardware design Proc. of the 32nd ACM\/IEEE conference on Design automation (DAC 95) 1995 pp.298\u2013303.","DOI":"10.1145\/217474.217545"},{"key":"e_1_2_11_11_1","doi-asserted-by":"crossref","unstructured":"S.Chandra P.Godefroid andC.Palm Software model checking in practice: An industrial case study Proc. of the 24th International Conference on Software Engineering (ICSE'02) 2002 pp.431\u2013441.","DOI":"10.1145\/581339.581393"},{"key":"e_1_2_11_12_1","doi-asserted-by":"crossref","unstructured":"D.Peled M. Y.Vardi andM.Yannakakis Black box checking Proc. of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification Testing and Verification (PSTV XIX) 1999 pp.225\u2013240.","DOI":"10.1007\/978-0-387-35578-8_13"},{"key":"e_1_2_11_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_11_14_1","doi-asserted-by":"crossref","unstructured":"K. L.McMillan Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits Proc. of the 4th International Workshop on Computer Aided Verification (CAV '92) 1993 pp.164\u2013177.","DOI":"10.1007\/3-540-56496-9_14"},{"key":"e_1_2_11_15_1","doi-asserted-by":"crossref","unstructured":"J.Esparza S.Romer andW.Vogler An improvement of mcmillan's unfolding algorithm Proc. of the 2nd International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '96) 1996 pp.87\u2013106.","DOI":"10.1007\/3-540-61042-1_40"},{"key":"e_1_2_11_16_1","doi-asserted-by":"crossref","unstructured":"M.Kaufmann M.Andrew andC.Pixley Design constraints in symbolic model checking Proc. of the 10th International Conference on Computer Aided Verification (CAV '98) 1998 pp.477\u2013487.","DOI":"10.1007\/BFb0028768"},{"volume-title":"Time and Modality","year":"1957","author":"Prior A.","key":"e_1_2_11_17_1"},{"key":"e_1_2_11_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001"},{"issue":"2","key":"e_1_2_11_19_1","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite\u2010state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke E. M.","year":"1986","journal-title":"ACM Trans. Programming Lang. Syst."},{"key":"e_1_2_11_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782772"},{"key":"e_1_2_11_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90041-Y"},{"key":"e_1_2_11_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"e_1_2_11_23_1","doi-asserted-by":"crossref","unstructured":"M.Ben\u2010Ari Z.Manna andA.Pnueli The temporal logic of branching time Proc. of the 8th ACM SIGPLAN\u2010SIGACT symposium on principles of programming languages (POPL'81) 1981 pp.164\u2013176.","DOI":"10.1145\/567532.567551"},{"key":"e_1_2_11_24_1","unstructured":"J. R.B\u00fcchi On a decision method in restricted second order arithmetic Proc. of the International Congress of Logic Methodology and Philosophy of Science 1960 pp.1\u201311."},{"key":"e_1_2_11_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)91258-X"},{"key":"e_1_2_11_26_1","unstructured":"M. Y.Vardi andP.Wolper An automata theoretic approach to automatic program verification Proc. of the 1st Symposium on Logic in Computer Science 1986 pp.332\u2013344."},{"volume-title":"Protocol Specification, Testing and Verification","year":"1995","author":"Gerth R.","key":"e_1_2_11_27_1"},{"key":"e_1_2_11_28_1","doi-asserted-by":"crossref","unstructured":"P.Gastin andD.Oddoux Fast LTL to B\u00fcchi automata translation Proc. of the 13th International Conference on Computer Aided Verification (CAV'01) 2001 pp.53\u201365.","DOI":"10.1007\/3-540-44585-4_6"},{"key":"e_1_2_11_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"},{"volume-title":"Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics","year":"1990","author":"Thomas W.","key":"e_1_2_11_30_1"},{"key":"e_1_2_11_31_1","unstructured":"H. W.Kamp Tense logic and the theory of linear order PhD thesis Los Angeles California UCLA 1968."},{"key":"e_1_2_11_32_1","doi-asserted-by":"crossref","unstructured":"D.Gabbay A.Pnueli S.Shelah andJ.Stavi On the temporal analysis of fairness Proc. of the 7th ACM SIGPLAN\u2010SIGACT symposium on Principles of programming languages (POPL '80) 1980 pp.163\u2013173.","DOI":"10.1145\/567446.567462"},{"volume-title":"Temporal Logic in Specification","year":"1987","author":"Gabbay D.","key":"e_1_2_11_33_1"},{"volume-title":"Handbook of Formal Languages, Vol. 3: Beyond Words","year":"1997","author":"Thomas W.","key":"e_1_2_11_34_1"},{"key":"e_1_2_11_35_1","doi-asserted-by":"crossref","unstructured":"F.Somenzi andR.Bloem Efficient B\u00fcchi automata from LTL formulae Proc. of the 12th International Conference on Computer Aided Verification(CAV'00) 2000 pp.248\u2013263.","DOI":"10.1007\/10722167_21"},{"key":"e_1_2_11_36_1","doi-asserted-by":"crossref","unstructured":"D.Giannakopoulou andF.Lerda From states to transitions: Improving translation of LTL formulae to B\u00fcchi automata Proc. of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems (FORTE '02) 2002 pp.308\u2013326.","DOI":"10.1007\/3-540-36135-9_20"},{"key":"e_1_2_11_37_1","doi-asserted-by":"crossref","unstructured":"R.Sebastiani andS.Tonetta \u201cMore deterministic\u201d vs. \u201csmaller\u201d B\u00fcchi automata for efficient LTL model checking Proc. of the the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2003) 2003 pp.126\u2013140.","DOI":"10.1007\/978-3-540-39724-3_12"},{"key":"e_1_2_11_38_1","unstructured":"M. Y.Vardi andP.Wolper An automata\u2010theoretic approach to automatic program verification (preliminary report) Proc. of Symposium on Logic in Computer Science (LICS'86) 1986 pp.332\u2013344."},{"key":"e_1_2_11_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"e_1_2_11_40_1","doi-asserted-by":"crossref","unstructured":"G. J.Holzmann D.Peled andM.Yannakakis On nested depth first search Proc. of 2nd SPIN Workshop. American Mathematical Society 1996.","DOI":"10.1090\/dimacs\/032\/03"},{"key":"e_1_2_11_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0104-3"},{"key":"e_1_2_11_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_11_43_1","unstructured":"O.Coudert C.Berthet andJ. C.Madre Verification of sequential machines using boolean functional vectors Proc. of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design 1989 pp.111\u2013128."},{"key":"e_1_2_11_44_1","doi-asserted-by":"crossref","unstructured":"P.Cousot andN.Halbwachs Automatic discovery of linear restraints among variables of a program Proc. of the 5th ACM SIGACT\u2010SIGPLAN symposium on Principles of programming languages (POPL '78) 1978 pp.84\u201396.","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_11_45_1","doi-asserted-by":"crossref","unstructured":"P.Cousot andR.Cousot Static determination of dynamic properties of programs Proc. of the 2nd International Symposium on Programming 1976 pp.106\u2013130.","DOI":"10.1145\/390018.808314"},{"key":"e_1_2_11_46_1","doi-asserted-by":"crossref","unstructured":"G.St\u00e5lmarck andM.S\u00e4fiund Modeling and verifying systems and software in propositional logic Proc. of Safety of Computer Control Systems Conference (SAFECOMP'90) 1990 pp.31\u201336.","DOI":"10.1016\/B978-0-08-040953-5.50011-8"},{"key":"e_1_2_11_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_11_48_1","doi-asserted-by":"crossref","unstructured":"A.Biere A.Cimatti E.Clarke andY.Zhu Symbolic model checking without BDDs Proc. of the 5th International Conference on Tools and Algorithms Construction and Analysis of system 1999 pp.193\u2013207.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_11_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_11_50_1","doi-asserted-by":"crossref","unstructured":"K. L.McMillan Symbolic model checking: an approach to the state explosion problem PhD thesis Kluver Academic 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"e_1_2_11_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.275352"},{"key":"e_1_2_11_52_1","doi-asserted-by":"crossref","unstructured":"E. A.Emerson andE. M.Clarke Characterizing correctness properties of parallel programs using fixpoints Proc. of the 7th Colloquium on Automata Languages and Programming 1980 pp.169\u2013181.","DOI":"10.1007\/3-540-10003-2_69"},{"key":"e_1_2_11_53_1","doi-asserted-by":"crossref","unstructured":"P.Godefroid andD.Pirottin Refining dependencies improves partial\u2010order verification methods (extended abstract) Proc. of the 5th International Conference on Computer Aided Verification (CAV '93) 1993 pp.438\u2013449.","DOI":"10.1007\/3-540-56922-7_36"},{"key":"e_1_2_11_54_1","doi-asserted-by":"crossref","unstructured":"D.Peled Combining partial order reductions with on\u2010the\u2010fly model\u2010checking Proc. of the 6th International Conference on Computer Aided Verification (CAV '94) 1994 377\u2013390.","DOI":"10.1007\/3-540-58179-0_69"},{"key":"e_1_2_11_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00709154"},{"key":"e_1_2_11_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90054-J"},{"key":"e_1_2_11_57_1","unstructured":"L.Lamport What good is temporal logic?Proc. of the IFIP 9th World Congress 1983 pp.657\u2013668."},{"key":"e_1_2_11_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(97)00133-6"},{"key":"e_1_2_11_59_1","doi-asserted-by":"crossref","unstructured":"D.Peled All from one one for all: On model checking using representatives Proc. of the 5th International Conference on Computer Aided Verification (CAV '93) 1993 pp.409\u2013423.","DOI":"10.1007\/3-540-56922-7_34"},{"key":"e_1_2_11_60_1","doi-asserted-by":"crossref","unstructured":"P.Godefroid Using partial orders to improve automatic verification methods Proc. of the 2nd International Workshop on Computer Aided Verification (CAV '90) 1991 pp.176\u2013185.","DOI":"10.1007\/BFb0023731"},{"key":"e_1_2_11_61_1","doi-asserted-by":"crossref","unstructured":"D.Bosnacki E.Elkind B.Genest andD.Peled On commutativity based edge lean search Proc. of the 34th Interantional Colloquium on Automata Languages and Programming (ICALP'97) 2007 pp.158\u2013170.","DOI":"10.1007\/978-3-540-73420-8_16"},{"volume-title":"Unfoldings \u2010 A Partial\u2010Order Approach to Model Checking","year":"2008","author":"Esparza J.","key":"e_1_2_11_62_1"},{"key":"e_1_2_11_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4176-8"},{"volume-title":"Computer Hardware Description Languages and their Applications","year":"1993","author":"Ip C. N.","key":"e_1_2_11_64_1"},{"key":"e_1_2_11_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/0141-9331(90)90047-Y"},{"key":"e_1_2_11_66_1","unstructured":"E. M.Clarke O.Grumberg H.Hiraishi S.Jha D. E.Long K. L.McMillan andL. A.Ness Verification of the Futurebus+ cache coherence protocol Proc. of the 11th International Symposium on Computer Hardware Description Languages and their Applications 1993 pp.5\u201320."},{"key":"e_1_2_11_67_1","unstructured":"E. A.Emerson andR. J.Trefler From asymmetry to full symmetry: New techniques for symmetry reduction in model checking Proc. of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME '99) 1999 pp.142\u2013156."},{"key":"e_1_2_11_68_1","doi-asserted-by":"crossref","unstructured":"S.Barner andO.Grumberg Combining symmetry reduction and under\u2010approximation for symbolic model checking Proc. of the 14th International Conference on Computer Aided Verification (CAV '02) 2002 pp.93\u2013106.","DOI":"10.1007\/3-540-45657-0_8"},{"key":"e_1_2_11_69_1","doi-asserted-by":"crossref","unstructured":"E. A.Emerson andA. P.Sistla Utilizing symmetry when model checking under fairness assumptions: an automata\u2010theoretic approach Proc. of the 7th International Conference on Computer Aided Verification (CAV'95) 1995 pp.309\u2013324.","DOI":"10.1007\/3-540-60045-0_59"},{"key":"e_1_2_11_70_1","doi-asserted-by":"crossref","unstructured":"A. P.Sistla andP.Godefroid Symmetry and reduced symmetry in model checking Proc. of the 13th International Conference on Computer Aided Verification (CAV '01) 2001 pp.91\u2013103.","DOI":"10.1007\/3-540-44585-4_9"},{"key":"e_1_2_11_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_11_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384313"},{"key":"e_1_2_11_73_1","doi-asserted-by":"crossref","unstructured":"M.Erne J.Koslowski A.Melton andG.Strecker A primer on galois connections Proc. of the 1991 Summer Conference on General Topology and Applications in Honor of Mary Ellen Rudin and Her Work 1993 pp.103\u2013125.","DOI":"10.1111\/j.1749-6632.1993.tb52513.x"},{"key":"e_1_2_11_74_1","doi-asserted-by":"crossref","unstructured":"P.Cousot Abstract interpretation: Theory and practice Proc. of the 9th International SPIN Workshop on Model Checking of Software 2002 pp.2\u20135.","DOI":"10.1007\/3-540-46017-9_2"},{"key":"e_1_2_11_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80004-0"},{"key":"e_1_2_11_76_1","doi-asserted-by":"crossref","unstructured":"T. A.Henzinger X.Nicollin J.Sifakis andS.Yovine Symbolic model checking for real\u2010time systems Proc. of the 7th Symposium of Logics in Computer Science (LICS '92) 1992 pp.394\u2013406.","DOI":"10.1109\/LICS.1992.185551"},{"key":"e_1_2_11_77_1","doi-asserted-by":"crossref","unstructured":"T. G.Rokicki andC. J.Myers Automatic verification of timed circuits Proc. of the 6th International Conference on Computer\u2010Aided Verification CAV'94 1994 pp.468\u2013480.","DOI":"10.1007\/3-540-58179-0_76"},{"key":"e_1_2_11_78_1","doi-asserted-by":"crossref","unstructured":"D.Dill Timing assumptions and verification of finite\u2010state concurrent systems Proc. of the International Workshop on Automatic Verification Methods for Finite State Systems 1990 pp.197\u2013212.","DOI":"10.1007\/3-540-52148-8_17"},{"key":"e_1_2_11_79_1","doi-asserted-by":"crossref","unstructured":"R.Alur C.Courcoubetis andD.Dill Model\u2010checking for real\u2010time systems Proc. of the 5th Annual IEEE Symp. on Logic in Computer Science (LICS'90) 1990 pp.414\u2013425.","DOI":"10.1109\/LICS.1990.113766"},{"key":"e_1_2_11_80_1","unstructured":"R.Alur Techniques for automatic verification of real\u2010time systems PhD thesis stanford CA Stanford University 1992."},{"volume-title":"Formal Methods for RealTime Computing. Trends in Software Series","year":"1996","author":"Alur R.","key":"e_1_2_11_81_1"},{"key":"e_1_2_11_82_1","doi-asserted-by":"crossref","unstructured":"A.Aziz V.Singhal R. K.Brayton andA. L.Sangiovanni\u2010Vincentelli It usually works: The temporal logic of stochastic systems Proc. of the 7th International Conference On Computer Aided Verification 1995 pp.155\u2013165.","DOI":"10.1007\/3-540-60045-0_48"},{"key":"e_1_2_11_83_1","doi-asserted-by":"crossref","unstructured":"C.Baier E.Clarke V.Hartonas\u2010Garmhausen andM.Kwiatkowska Symbolic model checking for probabilistic processes Proc. of the 24th Interantional Colloquium on Automata Languages and Programming (ICALP'97) 1997.","DOI":"10.1007\/3-540-63165-8_199"},{"key":"e_1_2_11_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_11_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"volume-title":"Advances in Computers","year":"2003","author":"Biere A.","key":"e_1_2_11_86_1"},{"key":"e_1_2_11_87_1","doi-asserted-by":"crossref","unstructured":"M. W.Moskewicz C. F.Madigan Y.Zhao L.Zhang andS.Malik Chaff: Engineering an efficient SAT solver Proc. of the 38th Design Automation Conference (DAC'01) 2001.","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_11_88_1","doi-asserted-by":"crossref","unstructured":"N.E\u00e9n andN.S\u00f6rensson An extensible sat\u2010solver Proc. of International Conference on Theory and Applications of Satisfiability testing (SAT) 2003 pp.502\u2013518.","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_2_11_89_1","doi-asserted-by":"crossref","unstructured":"S. A.Cook The complexity of theorem\u2010proving procedures Proc. of the 3rd annual ACM symposium on Theory of computing (STOC '71) 1971 pp.151\u2013158.","DOI":"10.1145\/800157.805047"},{"key":"e_1_2_11_90_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"e_1_2_11_91_1","doi-asserted-by":"crossref","unstructured":"M.Sheeran S.Singh andG.Staalmarck Checking safety properties using induction and a sat\u2010solver Proc. of the 3rd International Conference on Formal Methods in Computer\u2010Aided Design (FMCAD '00) 2000 pp.108\u2013125.","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_2_11_92_1","doi-asserted-by":"crossref","unstructured":"O.Shtrichman Pruning techniques for the SAT\u2010based bounded model checking problem Proc. of the 40thConference on Design Automation 2001 pp.58\u201370.","DOI":"10.1007\/3-540-44798-9_4"},{"key":"e_1_2_11_93_1","unstructured":"J. R.Burch E. M.Clarke andD. E.Long Symbolic model checking with partitioned transition relations Proc. of the International Conference on Very Large Scale Integration (VLSI '91) 1990."},{"key":"e_1_2_11_94_1","unstructured":"S. V.Campos A quantitative approach to the formal verification of realtime system PhD thesis SCS Pittsburgh PA: Carnegie Mellon University 1996."},{"key":"e_1_2_11_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"e_1_2_11_96_1","article-title":"In transition for global to modular temporal reasoning about programs","author":"Pnueli A.","year":"1984","journal-title":"Logics Models Concurrent Syst."},{"key":"e_1_2_11_97_1","unstructured":"M.Caporuscio P.Inverardi andP.Pelliccione Compositional verification of middleware\u2010based software architecture descriptions Proc. of the International Conference on Software Engineering (ICSE 2004) 2004."},{"key":"e_1_2_11_98_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-005-2641-y"},{"volume-title":"The SPIN Model Checker: Primer and Reference Manual","year":"2003","author":"Holzmann G. J.","key":"e_1_2_11_99_1"},{"key":"e_1_2_11_100_1","doi-asserted-by":"crossref","unstructured":"A.Cimatti E. M.Clarke F.Giunchiglia andM.Roveri NUSMV: A new symbolic model verifier Proc. of the 11th International Conference on Computer Aided Verification (CAV) 1999 pp.495\u2013499.","DOI":"10.1007\/3-540-48683-6_44"},{"key":"e_1_2_11_101_1","doi-asserted-by":"publisher","DOI":"10.1145\/949952.940107"}],"container-title":["Wiley Encyclopedia of Computer Science and Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/9780470050118.ecse247","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T03:12:42Z","timestamp":1738984362000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/9780470050118.ecse247"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,16]]},"ISBN":["9780471383932","9780470050118"],"references-count":100,"alternative-id":["10.1002\/9780470050118.ecse247","10.1002\/9780470050118"],"URL":"https:\/\/doi.org\/10.1002\/9780470050118.ecse247","archive":["Portico"],"relation":{},"subject":[],"published":{"date-parts":[[2009,3,16]]}}}