{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:04:42Z","timestamp":1754481882121},"reference-count":38,"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)80004-0","type":"journal-article","created":{"date-parts":[[2005,5,20]],"date-time":"2005-05-20T13:21:17Z","timestamp":1116595277000},"page":"417-432","source":"Crossref","is-referenced-by-count":25,"title":["Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach"],"prefix":"10.1016","volume":"89","author":[{"given":"Sagar","family":"Chaki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karen","family":"Yorav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80004-0_BIB1","unstructured":"BLAST website. http:\/\/www-cad.eecs.berkeley.edu\/~rupak\/blast."},{"key":"10.1016\/S1571-0661(05)80004-0_BIB2","unstructured":"MAGIC website. http:\/\/www.cs.cmu.edu\/~chaki\/magic."},{"key":"10.1016\/S1571-0661(05)80004-0_BIB3","unstructured":"SLAM website. http:\/\/research.microsoft.com\/slam."},{"key":"10.1016\/S1571-0661(05)80004-0_BIB4","series-title":"Proceedings of POPL","first-page":"191","article-title":"Compiling path expressions into VLSI circuits","author":"Anantharaman","year":"1985"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB5","series-title":"SIGPLAN Conference on Programming Language Design and Implementation","first-page":"203","article-title":"Automatic predicate abstraction of C programs","author":"Ball","year":"2001"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB6","first-page":"103","article-title":"Automatically validating temporal safety properties of interfaces","volume":"volume 2057","author":"Ball","year":"2001"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB7","first-page":"319","article-title":"Computing abstractions of infinite state systems compositionally and automatically","volume":"volume 1427","author":"Bensalem","year":"1998"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB8","series-title":"Trace algebra for automatic verification of real-time concurrent systems, PhD thesis","author":"Burch","year":"1992"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB9","series-title":"Proceedings of ICSE.","article-title":"Modular verification of software components in C","author":"Chaki","year":"2003"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB10","series-title":"Proceedings of FMCAD","first-page":"33","article-title":"Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis","author":"Chauhan","year":"2002"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB11","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB12","first-page":"52","article-title":"Synthesis of synchronization skeletons from branching time temporal logic","volume":"volume 131","author":"Clarke","year":"1982"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB13","first-page":"154","article-title":"Counterexample-guided abstraction refinement","volume":"volume 1855","author":"Clarke","year":"2000"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB14","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","author":"Clarke","year":"1994","journal-title":"Proceedings of TOPLAS"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB15","series-title":"Proceedings of CAV","first-page":"265","article-title":"SAT based abstraction-refinement using ILP and machine learning techniques","author":"Clarke","year":"2002"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB16","first-page":"331","article-title":"Learning assumptions for compositional verification","volume":"volume 2619","author":"Cobleigh","year":"2003"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB17","first-page":"293","article-title":"Generating finite-state abstractions of reactive systems using decision procedures","author":"Col\u00f3n","year":"1998","journal-title":"Proceedings of CAV"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB18","series-title":"Proceedings of ICSE","first-page":"439","article-title":"Bandera: extracting finite-state models from Java source code","author":"Corbett","year":"2000"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB19","series-title":"Proceedings of the SIGPLAN Conference on Programming Languages","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"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB20","article-title":"Shape analysis through predicate abstraction and model checking","volume":"volume 2575","author":"Dams","year":"2003"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB21","first-page":"160","article-title":"Experience with predicate abstraction","volume":"volume 1633","author":"Das","year":"1999"},{"issue":"3","key":"10.1016\/S1571-0661(05)80004-0_BIB22","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","article-title":"Model checking and modular verification. ACM Trans. on","volume":"16","author":"Grumberg","year":"1994","journal-title":"Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB23","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer. Thread-modular abstraction refinement. In Proceedings of CAV (to appear). Springer LNCS, 2003.","DOI":"10.1007\/978-3-540-45069-6_27"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB24","series-title":"Proceedings of POPL","first-page":"58","article-title":"Lazy abstraction","author":"Henzinger","year":"2002"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB25","series-title":"Proceedings of ICCAD","first-page":"245","article-title":"Decomposing refinement proofs using assume-guarantee reasoning","author":"Henzinger","year":"2000"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB26","series-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB27","first-page":"414","article-title":"Analysis of discrete event coordination","volume":"volume 430","author":"Kurshan","year":"1989"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB28","series-title":"Computer-aided verification of coordinating processes: the automata-theoretic approach","author":"Kurshan","year":"1994"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB29","first-page":"98","article-title":"Incremental verification by abstraction","volume":"volume 2031","author":"Lakhnech","year":"2001"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB30","first-page":"24","article-title":"A compositional rule for hardware design refinement","volume":"volume 1254","author":"McMillan","year":"1997"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB31","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB32","first-page":"435","article-title":"Syntactic program transformations for automatic abstraction","volume":"volume 1855","author":"Namjoshi","year":"2000"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB33","series-title":"Proceedings of ICSE","first-page":"594","article-title":"Verification of concurrent software with FLAVERS","author":"Naumovich","year":"1997"},{"issue":"6","key":"10.1016\/S1571-0661(05)80004-0_BIB34","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","article-title":"Three partition refinement algorithms","volume":"16","author":"Paige","year":"1987","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB35","first-page":"284","article-title":"Finding feasible countere-examples when model checking abstracted Java programs","volume":"volume 2031","author":"P\u01ces\u01cereanu, M. B. Dwyer","year":"2001"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB36","series-title":"The Theory and Practice of Concurrency","author":"Roscoe","year":"1997"},{"key":"10.1016\/S1571-0661(05)80004-0_BIB37","first-page":"72","article-title":"Construction of abstract state graphs with PVS","volume":"volume 1254","author":"Graf","year":"1997"},{"issue":"1","key":"10.1016\/S1571-0661(05)80004-0_BIB38","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/s10009-002-0077-2","article-title":"Model-checking multi-threaded distributed Java programs","volume":"4","author":"Stoller","year":"2002","journal-title":"International Journal on Software Tools for Technology Transfer"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800040?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800040?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T10:50:27Z","timestamp":1548499827000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105800040"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066105800040"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80004-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}