{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:32:12Z","timestamp":1720625532217},"reference-count":19,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2001,6,1]],"date-time":"2001-06-01T00:00:00Z","timestamp":991353600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"vor","delay-in-days":4920,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,6]]},"DOI":"10.1016\/s1571-0661(04)00151-3","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T05:34:35Z","timestamp":1075959275000},"page":"90-107","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Refining and Compressing Abstract Model Checking1 1The work is partially supported by MURST project: Certificazione automatica di programmi mediante interpretazione astratta."],"prefix":"10.1016","volume":"48","author":[{"given":"Agostino","family":"Dovier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Giacobazzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elisa","family":"Quintarelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB1","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finitestate concurrent system using temporal logic specification","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB2","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB3","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/239912.239914","article-title":"Complementation in Abstract Interpretation","volume":"19","author":"Cortesi","year":"1997","journal-title":"toplas"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB4","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1145\/234528.234740","article-title":"Abstract Interpretation","volume":"28","author":"Cousot","year":"1996","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB5","doi-asserted-by":"crossref","unstructured":"Cousot P. and R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Conference Record of the 4th ACM Symposioum on Principles of Programming Languages (POPL '77) (1977), pp. 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Cousot P. and R. Cousot, Systematic design of program analysis frameworks, in: Conference Record of the 6th ACM Symposioum on Principles of Programming Languages (POPL '79) (1979), pp. 269\u2013282.","DOI":"10.1145\/567752.567778"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Cousot P. and R. Cousot, Inductive definitions, semantics and abstract interpretation, in: Conference Record of the 19th ACM Symposioum on Principles of Programming Languages (POPL '92) (1992), pp. 83\u201394.","DOI":"10.1145\/143165.143184"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB8","doi-asserted-by":"crossref","unstructured":"Cousot P. and R. Cousot, Temporal abstract interpretation, in: Conference Record of the ACM Symposioum on Principles of Programming Languages (POPL '2000) (2000), pp. 12\u201325.","DOI":"10.1145\/325694.325699"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB9","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 Transaction on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB10","series-title":"\u201cIntroduction to Lattices and Order\u201d","author":"Davey","year":"1990"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB11","series-title":"Handbook of Theoretical Computer Science, B: Formal Models and Semantics","first-page":"997","article-title":"Temporal and modal logic","author":"Emerson","year":"1990"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB12","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/234528.234742","article-title":"A unifying view of abstract domain design","volume":"28","author":"Fil\u00e9","year":"1996","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB13","unstructured":"Fil\u00e9, G. and F. Ranzato, Complementation of abstract domains made easy, in: M. Maher, editor, Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming (JICSLP '96) (1996), pp. 348\u2013362."},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB14","doi-asserted-by":"crossref","unstructured":"Giacobazzi R. and F. Ranzato, Refining and compressing abstract domains, in: P. Degano, R. Gorrieri and A. Marchetti-Spaccamela, editors, Proceedings of the 24th International Colloqium on Automata, Languages and Programming (ICALP '97), Lecture Notes in Computer Science 1256 (1997), pp. 771\u2013781.","DOI":"10.1007\/3-540-63165-8_230"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB15","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0167-6423(97)00034-8","article-title":"Optimal domains for disjunctive abstract interpretation","volume":"32","author":"Giacobazzi","year":"1998","journal-title":"Science of Computing Programming"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB16","doi-asserted-by":"crossref","first-page":"1067","DOI":"10.1145\/293677.293680","article-title":"A logical model for relational abstract domains","volume":"20","author":"Giacobazzi","year":"1998","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB17","doi-asserted-by":"crossref","unstructured":"Jensen T., Disjunctive strictness analysis, in: Proceedings of the 7th IEEE Symposium on Logic in Computer Science (LICS '92) (1992), pp. 174\u2013185.","DOI":"10.1109\/LICS.1992.185531"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB18","series-title":"\u201cThe Temporal Logic of Reactive and Concurrent Systems\u201d","author":"Manna","year":"1992"},{"key":"10.1016\/S1571-0661(04)00151-3_NEWBIB19","unstructured":"M\u00fcller-Olm M., D. Schmidt and B. Steffen, Model-checking. A tutorial introduction, in: G. Fil\u00e9, editor, Proceedings of the International Static Analysis Symposium (SAS '99), Lecture Notes in Computer Science 1694 (1999), pp. 330\u2013354."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001513?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001513?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,15]],"date-time":"2019-02-15T01:57:27Z","timestamp":1550195847000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104001513"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,6]]},"references-count":19,"alternative-id":["S1571066104001513"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00151-3","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,6]]}}}