{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:08:29Z","timestamp":1761610109362,"version":"build-2065373602"},"reference-count":20,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3893,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1016\/s1571-0661(04)80401-8","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"17-32","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Tool for Abstraction in Model Checking"],"prefix":"10.1016","volume":"66","author":[{"given":"Mar\u00eda del Mar","family":"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":"78","reference":[{"issue":"2","key":"10.1016\/S1571-0661(04)80401-8_NEWBIB1","doi-asserted-by":"crossref","DOI":"10.1145\/5397.5399","article-title":"Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM TOPLAS"},{"issue":"5","key":"10.1016\/S1571-0661(04)80401-8_NEWBIB2","doi-asserted-by":"crossref","first-page":"1245","DOI":"10.1145\/186025.186051","article-title":"Model Checking and Abstraction","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM TOPLAS"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB3","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith. Counterexample-guided Abstraction Refinement, Proc. of the 12th CAV, LNCS-1855, pp. 154\u2013169, (2000).","DOI":"10.1007\/10722167_15"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB4","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, S.P. Iyer and D. Yankelevich. Optimality and abstraction in model checking. In A. Mycroft, editor, Static Analysis Symposium, LNCS-983, pp. 51\u201363, (1995)","DOI":"10.1007\/3-540-60360-3_32"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB5","first-page":"238","article-title":"Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints","author":"Cousot","year":"1977","journal-title":"Conf. Record of the 4th ACM Symp. on POPL"},{"issue":"2","key":"10.1016\/S1571-0661(04)80401-8_NEWBIB6","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","article-title":"Abstract Interpretation of Reactive Systems","volume":"19","author":"Dams","year":"1997","journal-title":"ACM TOPLAS"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB7","first-page":"14","article-title":"Abstraction in Software Model Checking: Principles and Practice","author":"Dams","year":"2002","journal-title":"9th Int. SPIN Workshop. Model Checking Software, LNCS-2318"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB8","unstructured":"G. Duval and T. Cattel. From Architecture down to Implementation of Safe Process Control Applications. Design, Verification and Simulation. In Proc. of the 13th Annual Hawaii Int. Conf. on System Sciences (HICSS 30) (1997)."},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB9","unstructured":"M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareau, W. Visser, H. Zheng. Tool-supported Program Abstraction for Finite-state Verification. Proc. of ICSE 2001, 2001."},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB10","doi-asserted-by":"crossref","unstructured":"M.M. Gallardo and P. Merino. A Framework for Automatic Construction of Abstract PROMELA Models. In Theoretical and Practical Aspects of Spin Model Checking, LNCS1680, pp. 184\u2013199, (1999)","DOI":"10.1007\/3-540-48234-2_15"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB11","unstructured":"M.M. Gallardo, P. Merino and E. Pimentel. Verifying Abstract LTL Properties on Concurrent Systems Proc. of the 6th World Conference on Integrated Design & Process Technology. (2002). To appear."},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB12","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, pp. 1021\u20131025 (2002).","DOI":"10.1145\/508791.508989"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB13","doi-asserted-by":"crossref","unstructured":"S. Graf. Verification of a distributed Cache Memory by using abstractions. In Dill, D., (Ed.) Computer Aided Verification, LNCS-818, pp. 207\u2013219, (1994).","DOI":"10.1007\/3-540-58179-0_55"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB14","unstructured":"S. Graf. Personal Communication. 2002."},{"issue":"4","key":"10.1016\/S1571-0661(04)80401-8_NEWBIB15","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","article-title":"Model Checking Java Programs using Java Path Finder","volume":"2","author":"Havelund","year":"2000","journal-title":"Software Tools for Technology Transfer (STTT)"},{"year":"1991","series-title":"Design and Validation of Comp. Protocolos","author":"Holzmann","key":"10.1016\/S1571-0661(04)80401-8_NEWBIB16"},{"issue":"5","key":"10.1016\/S1571-0661(04)80401-8_NEWBIB17","article-title":"The Model Checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Trans. on SE"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB18","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann and M. H. Smith. A Practical Method for the Verification of Event Driven Systems. In Proc. of ICSE99, pp. 597\u2013608, (1999).","DOI":"10.1145\/302405.302710"},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB19","unstructured":"W3Consortium. Extensible Markup Language (XML) 1.0 (Second Edition), available in: http:\/\/www.w3.org\/XML\/, (2000)."},{"key":"10.1016\/S1571-0661(04)80401-8_NEWBIB20","unstructured":"aSpin project. University of M\u00e1laga. http:\/\/www.lcc.uma.es\/~gisum\/fmse\/tools"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804018?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804018?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:05:11Z","timestamp":1761609911000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104804018"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["S1571066104804018"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80401-8","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A Tool for Abstraction in Model Checking","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80401-8","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}