{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T01:30:31Z","timestamp":1648690231360},"reference-count":21,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"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":3619,"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":[[2003,9]]},"DOI":"10.1016\/s1571-0661(05)80003-9","type":"journal-article","created":{"date-parts":[[2005,5,20]],"date-time":"2005-05-20T13:21:17Z","timestamp":1116595277000},"page":"405-416","source":"Crossref","is-referenced-by-count":3,"title":["Comparing Abstraction Refinement Algorithms"],"prefix":"10.1016","volume":"89","author":[{"given":"Dennis","family":"Dams","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80003-9_BIB1","first-page":"158","article-title":"Relative completeness of abstraction refinement for software model checking","volume":"2280","author":"Ball","year":"2002"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB2","doi-asserted-by":"crossref","unstructured":"Clarke, E., O. Grumberg, S. Jha, Y. Lu and H. Veith, Counterexample-guided abstraction refinement, in: Emerson and Sistla [8], pp. 154-169.","DOI":"10.1109\/TIME.2003.1214874"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB3","series-title":"Computer Aided Verification, number 697 in LNCS","first-page":"479","article-title":"Generation of reduced models for checking fragments of CTL","author":"Dams","year":"1993"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB4","series-title":"Verification, Model Checking, and Abstract Interpretation (VMCAI)","first-page":"310","article-title":"Shape analysis through predicate abstraction and model checking","author":"Dams","year":"2003"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB5","series-title":"\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","author":"Dams","year":"1996"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB6","series-title":"Computer Aided Verification","first-page":"160","article-title":"Experience with predicate abstraction","author":"Das","year":"1999"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB7","series-title":"\u201cModel Checking,\u201d","author":"Clarke","year":"2000"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB8","series-title":"\u201cComputer Aided Verification,\u201d","year":"2000"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB9","series-title":"Protocol Specification Testing and Verification","first-page":"3","article-title":"Simple on-the-fly automatic verification of linear temporal logic","author":"Gerth","year":"1995"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB10","series-title":"Computer Aided Verification, number 1254 in LNCS","first-page":"72","article-title":"Construction of abstract state graphs with PVS","author":"Graf","year":"1997"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB11","series-title":"POPL","first-page":"58","article-title":"Lazy abstraction","author":"Henzinger","year":"2002"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB12","first-page":"203","article-title":"Verification by augmented finitary abstraction","volume":"163","author":"Kesten","year":"2000"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB13","series-title":"\u201cComputer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach,\u201d Princeton Series in Computer Science","author":"Kurshan","year":"1994"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB14","first-page":"98","article-title":"Incremental verification by abstraction","volume":"2031","author":"Lakhnech","year":"2001"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB15","series-title":"Twelfth Annual ACM Symposium on Principles of Programming Languages","first-page":"97","article-title":"Checking that finite state concurrent programs satisfy their linear specification","author":"Lichtenstein","year":"1985"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB16","series-title":"\u201cThe Temporal Logic of Reactive and Concurrent Systems: Specification,\u201d","author":"Manna","year":"1992"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB17","series-title":"Computer Aided Verification, number 2725 in LNCS","first-page":"288","article-title":"Abstraction for branching time properties","author":"Namjoshi","year":"2003"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB18","doi-asserted-by":"crossref","unstructured":"Namjoshi, K. S. and R. P. Kurshan, Syntactic program transformations for automatic abstraction, in: Emerson and Sistla [8], pp. 435-449.","DOI":"10.1007\/10722167_33"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB19","series-title":"invited talk at the Fourth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI)","article-title":"Software model checking with abstraction refinement","author":"Podelski","year":"2002"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB20","doi-asserted-by":"crossref","unstructured":"Sipma, H. B., T. E. Uribe and Z. Manna, Deductive model checking, in: R. Alur and T. A. Henzinger, editors, Proceedings of the Eighth International Conference on Computer Aided Verification, number 1102 in LNCS (1996), pp. 208-219.","DOI":"10.1007\/3-540-61474-5_70"},{"key":"10.1016\/S1571-0661(05)80003-9_BIB21","series-title":"\u201cAbstraction-based Deductive-Algorithmic Verification of Reactive Systems,\u201d Ph.D. thesis, Computer Science Department, Stanford University, technical report STAN-CS-TR-99-1618","author":"Uribe","year":"1998"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800039?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800039?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T05:14:27Z","timestamp":1550726067000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105800039"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066105800039"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80003-9","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}