{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T13:57:02Z","timestamp":1789999022060,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540434771","type":"print"},{"value":"9783540460176","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46017-9_24","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:13Z","timestamp":1269897133000},"page":"254-257","source":"Crossref","is-referenced-by-count":7,"title":["\u03b1SPIN: Extending SPIN with Abstraction"],"prefix":"10.1007","author":[{"given":"Mar\u00eda","family":"del Mar Gallardo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jes\u00fas","family":"Mart\u00ednez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ernesto","family":"Pimentel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,5,23]]},"reference":[{"issue":"5","key":"24_CR1","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Trans. on Programming Languages and Systems, 16(5):1512\u20131245, 1994.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareau, W. Visser, H. Zheng. Tool-supported Program Abstraction for Finite-state Verification. Proc. Int. Conf. on Software Engineering, ICSE 2001, 2001.","DOI":"10.1109\/ICSE.2001.919092"},{"issue":"2","key":"24_CR3","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253\u2013291, 1997.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-48234-2_15","volume-title":"Theoretical and Practical Aspects of spin Model Checking","author":"M.M. Gallardo","year":"1999","unstructured":"M.M. Gallardo and P. Merino. A framework for automatic construction of abstract promela models. Theoretical and Practical Aspects of spin Model Checking, LNCS-1680:184\u2013199, 1999."},{"key":"24_CR5","unstructured":"M.M. Gallardo and P. Merino. A practical method to integrate abstractions into SDL and MSC based tools. In Proc. of the 5th Int. ERCIM Workshop on Formal Methods for Industrial Critical Systems, GMD Report 91, pages 84\u201389, 2000."},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"M.M. Gallardo, J. Martinez, P. Merino and E. Rosales, Using XML to implement Abstraction for Model Checking. In Proc. of ACM Symposium on Applied Computing, 2002.","DOI":"10.1145\/508791.508989"},{"key":"24_CR7","unstructured":"M.M. Gallardo, P. Merino, and E. Pimentel. Abstract satisfiability of linear temporal logic. In Proc. of I Jornadas sobre Programacion y Lenguajes, pages 163\u2013178, 2001."},{"key":"24_CR8","unstructured":"M.M. Gallardo, J. Martinez, P. Merino and E. Pimentel. \u03b1spin project. University of M\u00e1laga. http:\/\/www.lcc.uma.es\/~gisum\/fmse\/tools."},{"issue":"4","key":"24_CR9","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund K., Pressburger T., Model Checking Java Programs using Java Path Finder. Software Tools for Technology Transfer (STTT) 2(4):366\u2013381, 2000.","journal-title":"Software Tools for Technology Transfer (STTT)"},{"issue":"5","key":"24_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann and M. H. Smith. A Practical Method for the Verification of Event Driven Systems. In Proc. Int. Conf. on Software Engineering, ICSE99, pages 597\u2013608, 1999.","DOI":"10.1145\/302405.302710"},{"key":"24_CR12","unstructured":"W3Consortium. Extensible Markup Language (XML) 1.0 (Second Edition), http:\/\/www.w3.org\/XML\/ , 2000."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46017-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:47:23Z","timestamp":1558982843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46017-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434771","9783540460176"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-46017-9_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}