{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,4]],"date-time":"2023-06-04T13:10:19Z","timestamp":1685884219596},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,12,10]],"date-time":"2010-12-10T00:00:00Z","timestamp":1291939200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2011,2]]},"DOI":"10.1007\/s11432-010-4150-2","type":"journal-article","created":{"date-parts":[[2010,12,10]],"date-time":"2010-12-10T06:43:05Z","timestamp":1291963385000},"page":"258-267","source":"Crossref","is-referenced-by-count":2,"title":["Competent predicate abstraction in model checking"],"prefix":"10.1007","volume":"54","author":[{"given":"Li","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"XiaoYu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"XiangYu","family":"Luo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,12,10]]},"reference":[{"key":"4150_CR1","first-page":"72","volume":"1254","author":"S. Graf","year":"1997","unstructured":"Graf S, Saidi H. Construction of abstract state graphs with PVS. In: CAV97, Haifa, Isreal, 1997, 1254: 72\u201383","journal-title":"CAV97, Haifa, Isreal"},{"key":"4150_CR2","first-page":"187","volume":"1166","author":"S. Das","year":"1999","unstructured":"Das S, Dill D, Park P. Experience with predicate abstraction. CAV99, 1999, 1166: 187\u2013201","journal-title":"Experience with predicate abstraction"},{"key":"4150_CR3","first-page":"122","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge, MA: The MIT Press, 1999. 122\u2013124"},{"key":"4150_CR4","unstructured":"Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fix points. In: POPL77, Los Angeles, California, 1977. 238\u2013252"},{"key":"4150_CR5","first-page":"11","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux C, Graf S, Sifakis J, et al. Property preserving abstractions for the verification of concurrent systems. J FMSD, 1995, 6: 11\u201344","journal-title":"J FMSD"},{"key":"4150_CR6","first-page":"137","volume":"2028","author":"F. Ranzato","year":"2001","unstructured":"Ranzato F. On the completeness of model checking. ESOP\u20192001, 2001, 2028: 137\u2013154","journal-title":"ESOP\u20192001"},{"key":"4150_CR7","first-page":"154","volume":"1855","author":"E. M. Clarke","year":"2000","unstructured":"Clarke E M, Grumberg O, Jha S, et al. Counterexample-guided abstraction refinement. CAV00, 2000, 1855: 154\u2013169","journal-title":"CAV00"},{"key":"4150_CR8","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume":"37","author":"T. A. Henzinger","year":"2002","unstructured":"Henzinger T A, Jhala R, Majumdar R, et al. Lazy abstraction. POPL 2002, 2002, 37: 58\u201370","journal-title":"POPL 2002"},{"key":"4150_CR9","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1145\/378795.378846","volume":"36","author":"T. Ball","year":"2001","unstructured":"Ball T, Majumdar R, Millstein T, et al. Automatic predicate abstraction of C programs. PLDI01, 2001, 36: 203\u2013213","journal-title":"PLDI01"},{"key":"4150_CR10","first-page":"388","volume":"2988","author":"T. Ball","year":"2004","unstructured":"Ball T, Cook B, Das S, et al. Refining approximations in software predicate abstraction. TACAS04, 2004, 2988: 388\u2013403","journal-title":"TACAS04"},{"key":"4150_CR11","first-page":"13","volume":"1770","author":"T. A. Henzinger","year":"2000","unstructured":"Henzinger T A, Majumdar R. A classification of symbolic transition systems. STACS00, 2000, 1770: 13\u201334","journal-title":"STACS00"},{"key":"4150_CR12","first-page":"127","volume":"4134","author":"D. A. Schmidt","year":"2006","unstructured":"Schmidt D A. Underapproximating predicate transformers. SAS06, 2006, 4134: 127\u2013143","journal-title":"SAS06"},{"key":"4150_CR13","first-page":"32","volume-title":"A Discipline of Programming","author":"E. W. Dijkstra","year":"1976","unstructured":"Dijkstra E W. A Discipline of Programming. Upper Saddle River, NJ: Prentice Hall 1976. 32\u201335"},{"key":"4150_CR14","first-page":"189","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M. Huth","year":"2001","unstructured":"Huth M, Ryan M. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge: Cambridge University Press, 2001. 189\u2013193"},{"key":"4150_CR15","first-page":"797","volume":"1","author":"M. Fitting","year":"1991","unstructured":"Fitting M. Kleene\u2019s logic, generalized. J LC, 1991, 1: 797\u2013810","journal-title":"J LC"},{"key":"4150_CR16","first-page":"2","volume":"3148","author":"D. Beyer","year":"2004","unstructured":"Beyer D, Chlipala A J, Henzinger T A, et al. The blast query language for software verification. SAS04, 2004, 3148: 2\u201318","journal-title":"SAS04"},{"key":"4150_CR17","first-page":"265","volume":"21","author":"D. S. Rosenblum","year":"1995","unstructured":"Rosenblum D S. A practical approach to programming with assertions. J IEEE TSE, 1995, 21: 265\u2013265","journal-title":"J IEEE TSE"},{"key":"4150_CR18","first-page":"1","volume":"3440","author":"K. L. McMillan","year":"2005","unstructured":"McMillan K L. Application of craig interpolants in model checking. APN05, 2005, 3440: 1\u201312","journal-title":"APN05"},{"key":"4150_CR19","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K. L. McMillan","year":"2005","unstructured":"McMillan K L. An interpolating theorem prover. J TCS, 2005, 345: 101\u2013121","journal-title":"J TCS"},{"key":"4150_CR20","unstructured":"Li L, He K D, Li J, et al. Jckecher: A software model checker. http:\/\/code.google.com\/p\/jchecker\/ ."},{"key":"4150_CR21","unstructured":"Blei D, Harrelson C, Jhala R, et al. Vampyre: a proof generating theorem prover. http:\/\/www.eecs.berkeley.edu\/~rupak\/Vampyre ."},{"key":"4150_CR22","unstructured":"Henzinger T A, Majumdar R, Beyer D, et al. BLAST: Berkeley lazy abstraction software verification tool. http:\/\/mtc.epfl.ch\/software-tools\/blast\/"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-010-4150-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-010-4150-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-010-4150-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,4]],"date-time":"2023-06-04T12:41:19Z","timestamp":1685882479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-010-4150-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,10]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,2]]}},"alternative-id":["4150"],"URL":"https:\/\/doi.org\/10.1007\/s11432-010-4150-2","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12,10]]}}}