{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:47:02Z","timestamp":1761929222856,"version":"3.28.0"},"reference-count":40,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1109\/icse.2003.1201217","type":"proceedings-article","created":{"date-parts":[[2004,6,22]],"date-time":"2004-06-22T16:27:43Z","timestamp":1087921663000},"page":"385-395","source":"Crossref","is-referenced-by-count":108,"title":["Modular verification of software components in C"],"prefix":"10.1109","author":[{"given":"S.","family":"Chaki","sequence":"first","affiliation":[]},{"given":"E.","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"A.","family":"Groce","sequence":"additional","affiliation":[]},{"given":"S.","family":"Jha","sequence":"additional","affiliation":[]},{"given":"H.","family":"Veith","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","article-title":"Experience with predicate abstraction","author":"das","year":"1999","journal-title":"Computer Aided Verification"},{"key":"35","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"article-title":"Techniques for program verification","year":"1980","author":"nelson","key":"36"},{"journal-title":"Model checking","year":"2000","author":"clarke","key":"18"},{"journal-title":"Communication and Concurrency","year":"1989","author":"milner","key":"33"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"journal-title":"Communicating and Mobile Systems The ?-Calculus","year":"1999","author":"milner","key":"34"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"39","article-title":"CVC: A cooperating validity checker","author":"stump","year":"0","journal-title":"Conference on Computer-Aided Verification 2002"},{"key":"13","first-page":"2057","article-title":"Automatically validating temporal safety properties of interfaces","author":"ball","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"key":"14","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","article-title":"Symbolic model checking without BDDs","volume":"1579","author":"biere","year":"1999","journal-title":"Lecture Notes in Computer Science"},{"key":"37","first-page":"72","article-title":"Construction of abstract state graphs with PVS. In O. Grumberg, editor","volume":"1254","author":"graf","year":"1997","journal-title":"Computer Aided Verification"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"article-title":"Uniform approaches to the verification of finite state systems","year":"1997","author":"shukla","key":"38"},{"key":"12","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","article-title":"Boolean and cartesian abstraction for model checking C programs","volume":"2031","author":"ball","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"key":"21","first-page":"177","article-title":"Tool-supported program abstraction for finite-state verification","author":"dwyer","year":"2001","journal-title":"International Conference on Software Engineering"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"40","article-title":"SATO: An efficient propositional prover","author":"zhang","year":"0","journal-title":"Conference on Automated Deduction 1997"},{"key":"22","article-title":"Checking system rules using system-specific, programmer-written compiler extensions","author":"engler","year":"0","journal-title":"Symposium on Operating Systems Design and Implementation 2000"},{"key":"23","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44585-4_22","article-title":"ICS: Integrated canonizer and solver","author":"filliatre","year":"2001","journal-title":"Computer-Aided Verification"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512539"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"29","first-page":"5","article-title":"Application specific higher order logic theorem proving","author":"kroening","year":"2002","journal-title":"Proc of the Verification Workshop - VERIFY'02"},{"year":"0","key":"3"},{"year":"0","key":"2"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(91)90006-B"},{"year":"0","key":"1"},{"journal-title":"Concurrency State models & Java programs","year":"2000","author":"magee","key":"30"},{"year":"0","key":"7"},{"year":"0","key":"6"},{"journal-title":"Hilbert's Tenth Problem","year":"1993","author":"matiyasevich","key":"32"},{"year":"0","key":"5"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"year":"0","key":"4"},{"year":"0","key":"9"},{"year":"0","key":"8"}],"event":{"name":"25th International Conference on Software Engineering, 2003. Proceedings.","start":{"date-parts":[[2003,5,10]]},"location":"Portland, OR, USA","end":{"date-parts":[[2003,5,10]]}},"container-title":["25th International Conference on Software Engineering, 2003. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8548\/27042\/01201217.pdf?arnumber=1201217","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T04:15:30Z","timestamp":1497586530000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1201217\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"references-count":40,"URL":"https:\/\/doi.org\/10.1109\/icse.2003.1201217","relation":{},"subject":[],"published":{"date-parts":[[2003]]}}}