{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:44:34Z","timestamp":1748493874038},"reference-count":20,"publisher":"Elsevier BV","issue":"6","license":[{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4076,"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":[[2002,6]]},"DOI":"10.1016\/s1571-0661(04)80478-x","type":"journal-article","created":{"date-parts":[[2004,9,28]],"date-time":"2004-09-28T19:29:25Z","timestamp":1096399765000},"page":"218-237","source":"Crossref","is-referenced-by-count":2,"title":["Predicate Abstraction for Dense Real-Time Systems1 1This research was supported by the National Science Foundation under grants CCR-00-82560 and CCR-00-86096 and by NASA Langley Research Center under contract B09060051 and Cooperative Agreement NCC-1-399 with Honeywell Minneapolis. Most of this research has been conducted while the first author was visiting SRI International, July\/August 2001."],"prefix":"10.1016","volume":"65","author":[{"given":"M.Oliver","family":"M\u00f6ller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria","family":"Sorea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB1","first-page":"414","article-title":"Model-checking for real-time systems","author":"Alur","year":"1990","journal-title":"5th Symp. on Logic in Computer Science (LICS 90)"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB3","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BFb0028755","article-title":"Computing abstractions of infinite state systems compositionally and automatically","volume":"1427","author":"Bensalem","year":"1998","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB4","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","article-title":"Counterexample-guided abstraction refinement","volume":"1855","author":"Clarke","year":"2000","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB5","doi-asserted-by":"crossref","unstructured":"Cousot P. and R. Cousot, Abstract intrepretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Conference Record of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, CA, 1977, pp. 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB6","unstructured":"Dams, D. R., \u201cAbstract Interpretation and Partition Refinement for Model Checking,\u201d Ph.D. thesis, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands (1996)."},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Das S. and D. L. Dill, Successive approximation of abstract transition relations, in: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS-01) (2001), pp. 51\u201360.","DOI":"10.1109\/LICS.2001.932482"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB8","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-60045-0_66","article-title":"Verification of real-time systems by successive over and under approximation","volume":"939","author":"Dill","year":"1995","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB9","unstructured":"Filli\u01cetre J.-C., S. Owre, H. Rue\u00df and N. Shankar, ICS: Integrated Canonization and Solving, in: G. Berry, H. Comon and A. Finkel, editors, Proceedings of CAV'2001, Lecture Notes in Computer Science 2102 (2001), pp. 246\u2013249."},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB10","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","article-title":"Construction of abstract state graphs with PVS","volume":"1254","author":"Graf","year":"1997","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB11","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB12","unstructured":"Kick A., \u201cGeneration of counterexamples and witnesses for the Mu-calculus,\u201d Ph.D. thesis, University of Karlsruhe, Germany (1996)."},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB13","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional \u03bc-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB14","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/3-540-45319-9_8","article-title":"Incremental verification by abstraction","volume":"2031","author":"Lachnech","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB15","doi-asserted-by":"crossref","unstructured":"M\u00f6ller, M. O., H. Rue\u00df and M. Sorea, Predicate abstraction for dense real-time systems, Technical Report BRICS-RS-01-44, Department of Computer Science, University of Aarhus, Denmark (2001), Available online at http:\/\/www.brics.dk\/RS\/01\/44\/.","DOI":"10.7146\/brics.v8i44.21704"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB16","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/10722167_33","article-title":"Syntactic program transformations for automatic abstraction","volume":"1855","author":"Namjoshi","year":"2000","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB17","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","article-title":"Abstract and model check while you prove","volume":"1633","author":"Sa\u00efdi","year":"1999","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB18","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1023\/A:1008734703554","article-title":"Analysis of timed systems using time-abstracting bisimulations","volume":"18","author":"Tripakis","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB19","unstructured":"Uribe, T. E., \u201cAbstraction-based Deductive-Algorithmic Verification of Reactive Systems,\u201d Ph.D. thesis, Computer Science Department, Stanford University (1998), technical report STAN-CS-TR-99-1618."},{"key":"10.1016\/S1571-0661(04)80478-X_NEWBIB20","doi-asserted-by":"crossref","unstructured":"Yovine, S., Model-checking timed automata, in: G. Rozenberg and F. Vaandrager, editors, Embedded Systems, number 1494 in Lecture Notes in Computer Science, 1998, pp. 114\u2013152.","DOI":"10.1007\/3-540-65193-4_20"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480478X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480478X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T06:52:22Z","timestamp":1585896742000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610480478X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,6]]},"references-count":20,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2002,6]]}},"alternative-id":["S157106610480478X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80478-x","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2002,6]]}}}