{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T21:10:23Z","timestamp":1781298623435,"version":"3.54.1"},"reference-count":30,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"12","license":[{"start":{"date-parts":[[2014,12,1]],"date-time":"2014-12-01T00:00:00Z","timestamp":1417392000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["61322202"],"award-info":[{"award-number":["61322202"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["61133001"],"award-info":[{"award-number":["61133001"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["61420106004"],"award-info":[{"award-number":["61420106004"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["2010CB328102"],"award-info":[{"award-number":["2010CB328102"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2014,12,1]]},"DOI":"10.1109\/tse.2014.2357442","type":"journal-article","created":{"date-parts":[[2014,9,11]],"date-time":"2014-09-11T18:56:01Z","timestamp":1410461761000},"page":"1206-1223","source":"Crossref","is-referenced-by-count":27,"title":["Making CEGAR More Efficient in Software Model Checking"],"prefix":"10.1109","volume":"40","author":[{"given":"Cong","family":"Tian","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhao","family":"Duan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606566"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214874"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2000.896460"},{"key":"ref12","first-page":"176","article-title":"Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation","author":"glusman","year":"0","journal-title":"Proc Conf Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2009.105"},{"key":"ref15","author":"kurshan","year":"0","journal-title":"Computer Aided Verificaton of Coordinating Processes"},{"key":"ref16","first-page":"337","article-title":"Specification and verification of concurrent systems in CESAR","author":"quielle","year":"1981","journal-title":"Proc 5th Int Symp Program"},{"key":"ref17","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48234-2_1","article-title":"Integrated formal verification: Using model checking with automated abstraction, invariant generation, and theorem proving","author":"rushby","year":"1999","journal-title":"Theoretical and Practical Aspects of SPIN Model Checking Proc 5th and 6th Int SPIN Workshops"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.873897"},{"key":"ref19","year":"0"},{"key":"ref28","article-title":"On-the-fly LTL model checking of C programs","author":"tian","year":"0"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384314"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"ref3","article-title":"Static partial order reduction","author":"kurshan","year":"1998","journal-title":"Proc Int Conf Tools and Algorithms Constr and Anal Syst"},{"key":"ref6","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"clarke","year":"1981","journal-title":"Logics of Programs Workshop"},{"key":"ref29","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","article-title":"The software model checker Blast: Applications to software engineering","volume":"9","author":"beyer","year":"0","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"ref5","author":"mcmillan","year":"0","journal-title":"Symbolic Model Checking"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref7","article-title":"Bounded model checking","volume":"58","author":"biere","year":"0","journal-title":"Advances in Computers"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19630090502"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.829807"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/3-540-36126-X_3","article-title":"Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis","author":"chauhan","year":"2002","journal-title":"Proc Formal Methods Comput -Aided Des"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"ref22","first-page":"235","article-title":"Software verification with BLAST","author":"henzinger","year":"0","journal-title":"10th Int SPIN Workshop on Model Checking Software"},{"key":"ref21","first-page":"35","article-title":"SLAM2: Static driver verification with under 4% false alarms","author":"ball","year":"2010","journal-title":"Proc Conf Formal Methods Comput -Aided Des"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0155-3"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_28"},{"key":"ref26","first-page":"184","article-title":"CPACHECKER: A tool for configurable software verification","author":"beyer","year":"0","journal-title":"Proc 23rd Int Conf Comput Aided Verification"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2009.105"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/6983476\/06895263.pdf?arnumber=6895263","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:01:12Z","timestamp":1642003272000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6895263\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,1]]},"references-count":30,"journal-issue":{"issue":"12"},"URL":"https:\/\/doi.org\/10.1109\/tse.2014.2357442","relation":{},"ISSN":["0098-5589","1939-3520"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,1]]}}}