{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T06:26:46Z","timestamp":1730269606062,"version":"3.28.0"},"reference-count":21,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008,4]]},"DOI":"10.1109\/ipdps.2008.4536430","type":"proceedings-article","created":{"date-parts":[[2008,6,6]],"date-time":"2008-06-06T12:44:52Z","timestamp":1212756292000},"page":"1-5","source":"Crossref","is-referenced-by-count":0,"title":["Verifying linked data structure implementations"],"prefix":"10.1109","author":[{"given":"Karen","family":"Zee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","first-page":"111","article-title":"theorem prover","volume":"15","author":"schulz","year":"2002","journal-title":"Journal of AI Communications"},{"key":"17","first-page":"748","article-title":"pvs: a prototype verification system","volume":"607","author":"owre","year":"1992","journal-title":"LNAI"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_18"},{"key":"16","article-title":"isabelle\/hol: a proof assistant for higher-order logic","volume":"2283","author":"nipkow","year":"2002","journal-title":"LNCS"},{"key":"13","first-page":"70","article-title":"translating higher-order problems to first-order clauses","author":"meng","year":"2006","journal-title":"ESCoR Empir Successful Comp Reasoning"},{"article-title":"techniques for program verification","year":"1981","author":"nelson","key":"14"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/347324.348031"},{"key":"12","article-title":"the krakatoa tool for certification of java\/javacard programs annotated in jml","author":"marche?","year":"2003","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"2","article-title":"formal system development with kiv","volume":"1783","author":"balser","year":"2000","journal-title":"LNCS"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-004-0058-x"},{"journal-title":"Modular Data Structure Verification","year":"2007","author":"kuncak","key":"10"},{"key":"7","article-title":"efficient e-matching for smt solvers","author":"de moura","year":"2007","journal-title":"CADE"},{"key":"6","article-title":"integrating static checking and interactive verification: supporting multiple theories and provers in verification","author":"chalin","year":"2005","journal-title":"Proceedings of Verified Software Tools Technologies and Experiences (VSTTE)"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"4","article-title":"smallfoot: modular automatic assertion checking with separation logic","author":"berdine","year":"2005","journal-title":"FMCO"},{"key":"9","article-title":"mona: monadic second-order logic in practice","volume":"1019","author":"henriksen","year":"1995","journal-title":"LNCS"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_12"}],"event":{"name":"Distributed Processing Symposium (IPDPS)","start":{"date-parts":[[2008,4,14]]},"location":"Miami, FL, USA","end":{"date-parts":[[2008,4,18]]}},"container-title":["2008 IEEE International Symposium on Parallel and Distributed Processing"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4519061\/4536075\/04536430.pdf?arnumber=4536430","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,16]],"date-time":"2017-03-16T13:46:06Z","timestamp":1489671966000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4536430\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,4]]},"references-count":21,"URL":"https:\/\/doi.org\/10.1109\/ipdps.2008.4536430","relation":{},"ISSN":["1530-2075"],"issn-type":[{"type":"print","value":"1530-2075"}],"subject":[],"published":{"date-parts":[[2008,4]]}}}