{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,6]],"date-time":"2026-01-06T13:06:04Z","timestamp":1767704764876},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2004,3,1]],"date-time":"2004-03-01T00:00:00Z","timestamp":1078099200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["STTT"],"published-print":{"date-parts":[[2004,3]]},"DOI":"10.1007\/s10009-003-0122-9","type":"journal-article","created":{"date-parts":[[2004,3,19]],"date-time":"2004-03-19T18:53:20Z","timestamp":1079722400000},"page":"165-184","source":"Crossref","is-referenced-by-count":18,"title":["\u03b1SPIN: A tool for abstract model checking"],"prefix":"10.1007","volume":"5","author":[{"given":"Mar\u00eda","family":"del Mar Gallardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jes\u00fas","family":"Mart\u00ednez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernesto","family":"Pimentel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,3,1]]},"reference":[{"key":"122_CR1","doi-asserted-by":"crossref","unstructured":"Ball T, Podelski A, Rajamani S (2001) Boolean and Cartesian abstractions for model checking C programs. In: Proceedings of TACAS01, Genova, Italy, 2\u20136 April 2001. Lecture notes in computer science, vol 2031. Springer, Berlin Heidelberg New York, pp 268\u2013283","DOI":"10.1007\/3-540-45319-9_19"},{"key":"122_CR2","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: Proceedings of POPL 2002, Portland, OR, 16\u201318 January 2002, pp 1\u20133","DOI":"10.1145\/503272.503274"},{"key":"122_CR3","unstructured":"Brat G, Havelund K, Park S, Visser W (2000) Java PathFinder \u2013 a second generation of a Java model checker. In: Proceedings of the Post-CAV\u201900 workshop on advances in verification, Chicago, 20 July 2000"},{"key":"122_CR4","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS 8(2):244\u2013263","journal-title":"ACM TOPLAS"},{"key":"122_CR5","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"Clarke","year":"1994","unstructured":"Clarke EM, Grumberg O, Long DE (1994) Model checking and abstraction. ACM TOPLAS 16(5):1512\u20131542","journal-title":"ACM TOPLAS"},{"key":"122_CR6","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th International Conference CAV\u201900, Chicago, 15\u201319 July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"122_CR7","unstructured":"Clarke E, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge, MA"},{"key":"122_CR8","doi-asserted-by":"crossref","unstructured":"Cleaveland R, Iyer SP, Yankelevich D (1995) Optimality and abstraction in model checking. In: Mycroft A (ed) Proceedings of the symposium on static analysis, Glasgow, 25\u201327 September 1995. Lecture notes in computer science, vol 983. Springer, Berlin Heidelberg New York, pp 51\u201363","DOI":"10.1007\/3-540-60360-3_32"},{"key":"122_CR9","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference record of the 4th ACM symposium on POPL, Los Angeles, January 1977, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"122_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"Dams","year":"1977","unstructured":"Dams D, Gerth R, Grumberg O (1977) Abstract interpretation of reactive systems. ACM TOPLAS 19(2):253\u2013291","journal-title":"ACM TOPLAS"},{"key":"122_CR11","doi-asserted-by":"crossref","unstructured":"Dams D (2002) Abstraction in software model checking: principles and practice. In: Proceedings of the 9th international SPIN workshop: model checking software, Grenoble, France, 11\u201313 April 2002. Lecture notes in computer science, vol 2318. Springer, Berlin Heidelberg New York, pp 14\u201321","DOI":"10.1007\/3-540-46017-9_4"},{"key":"122_CR12","doi-asserted-by":"crossref","unstructured":"Dams D, Hesse W, Holzmann GJ (2002) Abstracting C with abC. In: Proceedings of the 14th international conference CAV\u201902, Copenhagen, 27\u201331 July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 515\u2013520","DOI":"10.1007\/3-540-45657-0_43"},{"key":"122_CR13","unstructured":"Duval G, Cattel T (1997) From architecture down to implementation of safe process control applications: design, verification and simulation. In: Proceedings of the 13th annual Hawaii international conference on system sciences (HICSS 30), Honolulu, 3\u20136 January 1997"},{"key":"122_CR14","doi-asserted-by":"crossref","unstructured":"Dwyer M, Hatcliff J, Joehanes R, Laubach S, Pasareanu C, Visser W, Zheng H (2001) Tool-supported program abstraction for finite-state verification. In: Proceedings of ICSE 2001, Toronto, 12\u201319 May 2001, pp 177\u2013187","DOI":"10.1109\/ICSE.2001.919092"},{"key":"122_CR15","doi-asserted-by":"crossref","unstructured":"Fersman E, Jonsson B (2000) Abstraction of communication channels in Promela: a case study. In: Proceedings of the 3rd international SPIN workshop, Stanford, CA, 31 August\u20131 September 2000, pp 187\u2013204","DOI":"10.1007\/10722468_12"},{"key":"122_CR16","doi-asserted-by":"crossref","unstructured":"Gallardo MM, Merino P (1999) A framework for automatic construction of abstract promela models. In: Theoretical and practical aspects of spin model checking. Lecture notes in computer science, vol 1680. Springer, Berlin Heidelberg New York, pp 184\u2013199","DOI":"10.1007\/3-540-48234-2_15"},{"key":"122_CR17","unstructured":"Gallardo MM, Merino P (2000) A practical method to integrate abstractions into SDL and MSC based tools. In: Proceedings of the 5th international ERCIM workshop on formal methods for industrial critical systems, Berlin, 3\u20134 April 2000. GMD Report 91, pp 84\u201389"},{"key":"122_CR18","unstructured":"Gallardo MM, Merino P, Pimentel E (2002) Verifying abstract LTL properties on concurrent systems. In: Proceedings of the 6th world conference on integrated design & process technology, Pasadena, CA, 23\u201328 June 2002"},{"key":"122_CR19","doi-asserted-by":"crossref","unstructured":"Gallardo MM, Martinez J, Merino P, Rosales E (2002) Using XML to implement abstraction for model checking. In: Proceedings of the ACM symposium on applied computing, Madrid, 10\u201312 March 2002, pp 1021\u20131025","DOI":"10.1145\/508791.508989"},{"key":"122_CR20","doi-asserted-by":"publisher","first-page":"101","DOI":"10.5381\/jot.2002.1.2.a1","volume":"1","author":"Gallardo","year":"2002","unstructured":"Gallardo MM, Merino P, Pimentel E (2002) Debugging UML designs with model checking. J Object Technol 1(2):101\u2013117","journal-title":"J Object Technol"},{"key":"122_CR21","doi-asserted-by":"crossref","unstructured":"Gallardo MM, Merino P, Pimentel E (2002) Comparing under and over-approximations of LTL properties for model checking. In: Proceedings of the 11h international workshop on functional and (constraint) logic programming, Grado, Italy, 20\u201322 June 2002. Electronic notes in theoretical computer science, vol 76. Elsevier, Amsterdam. Available at: http:\/\/www.elsevier.nl\/gej-ng\/31\/29\/23\/show\/Products\/notes\/index.htt","DOI":"10.1016\/S1571-0661(04)80790-4"},{"key":"122_CR22","doi-asserted-by":"crossref","unstructured":"Gallardo MM, Mart\u00ednez J, Merino P, Pimentel E (2002) A tool for abstraction in model checking. In: Proceedings of the 7th international workshop on formal methods for industrial critical systems, M\u00e1laga, 12-13 July 2002. Electronic notes in theoretical computer science, 66(2). Elsevier, Amsterdam. Available at: http:\/\/www.elsevier.nl\/gej-ng\/31\/29\/23\/show\/Products\/notes\/index.htt","DOI":"10.1016\/S1571-0661(04)80401-8"},{"key":"122_CR23","doi-asserted-by":"crossref","unstructured":"Gallardo MM, Merino P, Pimentel E (2002) Refinement of LTL formulas for abstract model checking. In: Proceedings of the 9th international static analysis symposium (SAS \u201902), Madrid, 17\u201320 September 2002. Lecture notes in computer science, vol 2477. Springer, Berlin Heidelberg New York, pp 395\u2013410","DOI":"10.1007\/3-540-45789-5_28"},{"key":"122_CR24","unstructured":"Gerth R, Peled D, Vardi M, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of the 15th workshop on protocol specification, testing, and verification (PSTV95), Warsaw, Poland, 13\u201316 June 1995, pp 3\u201318"},{"key":"122_CR25","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"Giacobazzi","year":"2000","unstructured":"Giacobazzi R, Ranzato F, Scozzari F (2000) Making abstract interpretation complete. J ACM 47(2):361\u2013416","journal-title":"J ACM"},{"key":"122_CR26","doi-asserted-by":"crossref","unstructured":"Giacobazzi R, Quintarelli E (2001) Incompleteness, counterexamples and refinement in abstract model-checking. In: Proceedings of the 8th international static analysis symposium (SAS\u201901), Paris, 16\u201318 July 2001. Lecture notes in computer science, vol 2126. Springer, Berlin Heidelberg New York, pp 356\u2013373","DOI":"10.1007\/3-540-47764-0_20"},{"key":"122_CR27","doi-asserted-by":"crossref","unstructured":"Gondow K, Kawashima H (2002) Towards ANSI C program slicing using XML. In: Proceedings of the 2nd workshop on language descriptions, tools and applications (LDTA 2002), Grenoble, France, 13 April 2002. Electronic notes in theoretical computer science, vol 65, no 3. Elsevier, Amsterdam. Available at: http:\/\/www.informatik.uni-trier.de\/\u223cley\/db\/journals\/entcs\/entcs65.html","DOI":"10.1016\/S1571-0661(04)80425-0"},{"key":"122_CR28","doi-asserted-by":"crossref","unstructured":"Graf S (1994) Verification of a distributed cache memory by using abstractions. In: Proceedings of the 6th international conference CAV\u201994, Stanford, CA, 21\u201323 June 1994. Lecture notes in computer science, vol 818. Springer, Berlin Heidelberg New York, pp 207\u2013219","DOI":"10.1007\/3-540-58179-0_55"},{"key":"122_CR29","doi-asserted-by":"crossref","unstructured":"Graf S, Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In: Proceedings of the 9th international conference CAV\u201997, Haifa, Israel, 22\u201325 June 1997. Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"122_CR30","unstructured":"Hatcliff J, Dwyer M, Pasareanu C, Robby (2003) Foundations of the Bandera abstraction tools. The essence of compution. Lecture notes in computer science, vol 2566. Springer, Berlin Heidelberg New York, pp 172\u2013203"},{"key":"122_CR31","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"Havelund","year":"2000","unstructured":"Havelund K, Pressburger T (2000) Model checking Java programs using Java Path Finder. Int J Softw Tools Technol Transfer 2(4):366\u2013381","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"122_CR32","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/s10009-002-0080-7","volume":"4","author":"Havelund","year":"2002","unstructured":"Havelund K, Visser W (2002) Program model checking as a new trend. Int J Softw Tools Technol Transfer 4:8\u201320","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"122_CR33","unstructured":"Holzmann GJ (1991) Design and validation of computer protocols. Prentice-Hall, Upper Saddle River, NJ"},{"key":"122_CR34","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5):279\u2013295","journal-title":"IEEE Trans Softw Eng"},{"key":"122_CR35","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (1999) The engineering of a model checker: the Gnu i-Protocol case study revisited. In: Theoretical and practical aspects of spin model checking, Lecture notes in computer science, vol 1680. Springer, Berlin Heidelberg New York, pp 156\u2013168","DOI":"10.1007\/3-540-48234-2_18"},{"key":"122_CR36","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s100090050039","volume":"2","author":"Holzmann","year":"2000","unstructured":"Holzmann GJ, Najm E, Serhrouchni A (2000) SPIN model checking: an introduction. Int J Softw Tools Technol Transfer 2:321\u2013327","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"122_CR37","unstructured":"Holzmann GJ, Smith MH (1999) A practical method for the verification of event driven systems. In: Proceedings of 21st International Conference on Software Engineering ICSE99, Los Angeles, 12\u201322 May 1999, pp 597\u2013608"},{"key":"122_CR38","first-page":"a","volume":"abstraction","author":"Kelb","year":"1994","unstructured":"Kelb P (1994) Model checking and abstraction: a framework preserving both truth and failure information. Tecnical Report OFFIS, University of Oldenburg, Germany","journal-title":"Model checking and"},{"key":"122_CR39","first-page":"203","volume":"Comput","author":"Kesten","year":"2000","unstructured":"Kesten Y, Pnueli A (2000) Verification by augmented finitary abstraction. Inf Comput (Special Issue on Compositionality 163:203\u2013243","journal-title":"Inf"},{"key":"122_CR40","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Kesten","year":"2000","unstructured":"Kesten Y, Pnueli A (2000) Control and data abstraction: the cornerstones of practical formal verification. Int J Softw Tools Technol Transfer 2:328\u2013342","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"122_CR41","first-page":"1","volume":"6","author":"Loiseaux","year":"1995","unstructured":"Loiseaux C, Graf S, Sifakis J, Bouajjani A, Bensalem S (1995) Property preserving abstractions for the verification of concurrent systems. Formal Meth Sys Des 6:1\u201335","journal-title":"Formal Meth Sys Des"},{"key":"122_CR42","doi-asserted-by":"crossref","unstructured":"Pasareanu CS, Dwyer MB, Visser W (2001) Finding feasible counter-examples when model checking abstracted Java programs. In: Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems, (TACAS 2001) Genova, 2\u20136 April 2001. Lecture notes in computer science, vol 2031, Springer, Berlin Heidelberg New York, pp 284\u2013298","DOI":"10.1007\/3-540-45319-9_20"},{"key":"122_CR43","doi-asserted-by":"crossref","unstructured":"Sa\u00efdi H (2000) Model checking guided abstraction and analysis. In: Proceedings of the 7th international static analysis symposium (SAS2000), Santa Barbara, 29 June\u20131 July 2000. Lecture notes in computer science, vol 1824. Springer, Berlin Heidelberg New York, pp 377\u2013396","DOI":"10.1007\/978-3-540-45099-3_20"},{"key":"122_CR44","doi-asserted-by":"crossref","unstructured":"Visser W, Havelund K, Brat G, Park S (2000) Model checking programs. In: Proceedings of the 15th IEEE conference on automated software engineering, Grenoble, France, 11\u201315 September 2000, pp 3\u201312","DOI":"10.1109\/ASE.2000.873645"},{"key":"122_CR45","unstructured":"W3Consortium. Extensible Markup Language (XML) 1.0, 2nd edn. Available at: http:\/\/www.w3.org\/XML\/"},{"key":"122_CR46","unstructured":"\u03b1spin project. University of M\u00e1laga. http:\/\/www.lcc.uma.es\/gisum\/fmse\/tools"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0122-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0122-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0122-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0122-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:18Z","timestamp":1559114718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0122-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,3]]},"references-count":46,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2004,3]]}},"alternative-id":["122"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0122-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,3]]}}}