{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,28]],"date-time":"2026-10-28T16:53:00Z","timestamp":1793206380315,"version":"4.5.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,6,9]],"date-time":"2014-06-09T00:00:00Z","timestamp":1402272000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Australian Government"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,6,9]]},"DOI":"10.1145\/2594291.2594296","type":"proceedings-article","created":{"date-parts":[[2014,5,13]],"date-time":"2014-05-13T08:18:34Z","timestamp":1399969114000},"page":"429-439","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Don't sweat the small stuff"],"prefix":"10.1145","author":[{"given":"David","family":"Greenaway","sequence":"first","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Japheth","family":"Lim","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[{"name":"NICTA and UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"1","volume-title":"20th ESOP","author":"Appel A.","year":"2011","unstructured":"A. Appel . Verified software toolchain . In 20th ESOP , volume 6602 of LNCS , pages 1 -- 17 . Springer , 2011 . A. Appel. Verified software toolchain. In 20th ESOP, volume 6602 of LNCS, pages 1--17. Springer, 2011."},{"key":"e_1_3_2_1_3_1","first-page":"35","volume-title":"2010 FMCAD","author":"Ball T.","year":"2010","unstructured":"T. Ball , E. Bounimova , R. Kumar , and V. Levin . SLAM2: Static driver verification with under 4% false alarms . In 2010 FMCAD , pages 35 -- 42 , Lugano, Switzerland , 2010 . FMCAD Inc. T. Ball, E. Bounimova, R. Kumar, and V. Levin. SLAM2: Static driver verification with under 4% false alarms. In 2010 FMCAD, pages 35--42, Lugano, Switzerland, 2010. FMCAD Inc."},{"key":"e_1_3_2_1_4_1","unstructured":"J. Bloch. Nearly all binary searches and mergesorts are broken. http:\/\/googleresearch.blogspot.com\/2006\/06\/extra-extra-read-all-about-it-nearly.html Jun 2006.  J. Bloch. Nearly all binary searches and mergesorts are broken. http:\/\/googleresearch.blogspot.com\/2006\/06\/extra-extra-read-all-about-it-nearly.html Jun 2006."},{"key":"e_1_3_2_1_5_1","series-title":"LNCS","first-page":"102","volume-title":"5th MPC","author":"Bornat R.","year":"2000","unstructured":"R. Bornat . Proving pointer programs in Hoare Logic . In 5th MPC , volume 1837 of LNCS , pages 102 -- 126 . Springer , Jul 2000 . R. Bornat. Proving pointer programs in Hoare Logic. In 5th MPC, volume 1837 of LNCS, pages 102--126. Springer, Jul 2000."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_1_10_1","unstructured":"D. Greenaway. Autocorres tool. http:\/\/ssrg.nicta.com.au\/projects\/TS\/autocorres\/ 2014.  D. Greenaway. Autocorres tool. http:\/\/ssrg.nicta.com.au\/projects\/TS\/autocorres\/ 2014."},{"key":"e_1_3_2_1_11_1","series-title":"LNCS","first-page":"99","volume-title":"3rd ITP","author":"Greenaway D.","year":"2012","unstructured":"D. Greenaway , J. Andronick , and G. Klein . Bridging the gap: Automatic verified abstraction of C . In 3rd ITP , volume 7406 of LNCS , pages 99 -- 115 , Princeton, New Jersey , Aug 2012 . Springer . D. Greenaway, J. Andronick, and G. Klein. Bridging the gap: Automatic verified abstraction of C. In 3rd ITP, volume 7406 of LNCS, pages 99--115, Princeton, New Jersey, Aug 2012. Springer."},{"key":"e_1_3_2_1_12_1","series-title":"LNCS","first-page":"235","volume-title":"10th SPIN","author":"Henzinger T. A.","year":"2003","unstructured":"T. A. Henzinger , R. Jhala , R. Majumdar , and G. Sutre . Software verification with Blast . In 10th SPIN , volume 2648 of LNCS , pages 235 -- 239 , Portland, OR , USA, May 2003 . Springer . T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In 10th SPIN, volume 2648 of LNCS, pages 235--239, Portland, OR, USA, May 2003. Springer."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_16_1","series-title":"LNCS","first-page":"332","volume-title":"3rd ITP","author":"Klein G.","year":"2012","unstructured":"G. Klein , R. Kolanski , and A. Boyton . Mechanised separation algebra . In 3rd ITP , volume 7406 of LNCS , pages 332 -- 337 . Springer , 2012 . G. Klein, R. Kolanski, and A. Boyton. Mechanised separation algebra. In 3rd ITP, volume 7406 of LNCS, pages 332--337. Springer, 2012."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","first-page":"121","volume-title":"19th CADE","author":"Mehta F.","year":"2003","unstructured":"F. Mehta and T. Nipkow . Proving pointer programs in higher-order logic . In 19th CADE , volume 2741 of LNCS , pages 121 -- 135 , 2003 . F. Mehta and T. Nipkow. Proving pointer programs in higher-order logic. In 19th CADE, volume 2741 of LNCS, pages 121--135, 2003."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_21_1","volume-title":"Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. Paulson , and M. Wenzel . Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic . Springer , 2002 . T. Nipkow, L. Paulson, and M. Wenzel. Isabelle\/HOL --- A Proof Assistant for Higher-Order Logic. Springer, 2002."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_4"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/363534.363554"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_26_1","volume-title":"Automatic Verification of Programs with Complex Data Structures","author":"Suzuki N.","year":"1980","unstructured":"N. Suzuki . Automatic Verification of Programs with Complex Data Structures . Garland Publishing , New York , 1980 . N. Suzuki. Automatic Verification of Programs with Complex Data Structures. Garland Publishing, New York, 1980."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/645580.658811"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2349896.2349905"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_34"}],"event":{"name":"PLDI '14: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Edinburgh United Kingdom","acronym":"PLDI '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","NSF"]},"container-title":["Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2594291.2594296","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2594291.2594296","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:01:04Z","timestamp":1750215664000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2594291.2594296"}},"subtitle":["formal verification of C code without the pain"],"short-title":[],"issued":{"date-parts":[[2014,6,9]]},"references-count":27,"alternative-id":["10.1145\/2594291.2594296","10.1145\/2594291"],"URL":"https:\/\/doi.org\/10.1145\/2594291.2594296","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2666356.2594296","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,6,9]]},"assertion":[{"value":"2014-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}