{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:32Z","timestamp":1750221272323,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,9,29]],"date-time":"2017-09-29T00:00:00Z","timestamp":1506643200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,9,29]]},"DOI":"10.1145\/3127041.3127061","type":"proceedings-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T12:34:00Z","timestamp":1506515640000},"page":"118-121","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Using the coq theorem prover to verify complex data structure invariants"],"prefix":"10.1145","author":[{"given":"Kenneth","family":"Roe","sequence":"first","affiliation":[{"name":"The Johns Hopkins University"}]},{"given":"Scott F.","family":"Smith","sequence":"additional","affiliation":[{"name":"The Johns Hopkins University"}]}],"member":"320","published-online":{"date-parts":[[2017,9,29]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Greg Morrisett Avraham Shinnar Ryan Wisnesky Adam Chlipala Gregory Malecha. Effective interactive proofs for higher-order imperative programs. 2009.  Greg Morrisett Avraham Shinnar Ryan Wisnesky Adam Chlipala Gregory Malecha. Effective interactive proofs for higher-order imperative programs. 2009."},{"key":"e_1_3_2_1_2_1","unstructured":"A. W. Appel. Tactics for separation logic 2006. Early draft.  A. W. Appel. Tactics for separation logic 2006. Early draft."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792236"},{"volume-title":"Third International Conference, ITP","year":"2012","author":"Bengtson Jesper","key":"e_1_3_2_1_4_1"},{"key":"e_1_3_2_1_5_1","first-page":"207","volume-title":"USENIX Security","volume":"15","author":"Beringer Lennart","year":"2015"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_9_1","unstructured":"David Costanzo Zhong Shao and Ronghui. End-to-end verification of information-flow security for c and assembly programs.  David Costanzo Zhong Shao and Ronghui. End-to-end verification of information-flow security for c and assembly programs."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11527695_23"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_2"},{"volume-title":"TACAS","year":"2006","author":"O'Hearn Dino Distefano Peter W.","key":"e_1_3_2_1_13_1"},{"volume-title":"Proceedings of Conference on Compiler Construction","year":"2002","author":"Rahul Westley Weimer S. P.","key":"e_1_3_2_1_14_1"},{"volume-title":"CAV'07","year":"2007","author":"Berdine B Cook D","key":"e_1_3_2_1_15_1"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"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","unstructured":"Huisong Li Franois Brenger Bor-Yuh Evan Chang and Xavier Rival. Semantic-directed clumping of disjunctive abstract states. page 13 pages 2017.  Huisong Li Franois Brenger Bor-Yuh Evan Chang and Xavier Rival. Semantic-directed clumping of disjunctive abstract states. page 13 pages 2017."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391479"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1881833.1881855"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"volume-title":"CAV","year":"2016","author":"Manevich Roman","key":"e_1_3_2_1_22_1"},{"issue":"2","key":"e_1_3_2_1_23_1","first-page":"304","article-title":"A certified verifier for a fragment of separation logic","volume":"4","author":"Marti Nicolas","year":"2009","journal-title":"Information and Media Technologies"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_22"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_24"},{"volume-title":"University of New Mexico","year":"2014","author":"Nguyen ThanhVu","key":"e_1_3_2_1_26_1"},{"key":"e_1_3_2_1_27_1","first-page":"1","volume-title":"Proceedings of CSL'01","volume":"2142","author":"Peter O'Hearn Hongseok Yang","year":"2001"},{"key":"e_1_3_2_1_28_1","unstructured":"Benjamin C. Pierce Chris Casinghino Michael Greenberg Vilhelm Sjberg and Brent Yorgey. Software Foundations. 2011.  Benjamin C. Pierce Chris Casinghino Michael Greenberg Vilhelm Sjberg and Brent Yorgey. Software Foundations. 2011."},{"key":"e_1_3_2_1_29_1","volume-title":"Computer Aided Verification. CAV. Lecture Notes in Computer Science","volume":"8044","author":"Piskac","year":"2013"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"volume-title":"ITP","year":"2016","author":"Roe Kenneth","key":"e_1_3_2_1_32_1"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271517"},{"key":"e_1_3_2_1_35_1","volume-title":"Static Analysis. SAS. Lecture Notes in Computer Science","volume":"2477","author":"Yavuz-Kahveci","year":"2002"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72734-7_26"}],"event":{"name":"MEMOCODE '17: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"],"location":"Vienna Austria","acronym":"MEMOCODE '17"},"container-title":["Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127041.3127061","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3127041.3127061","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:07Z","timestamp":1750212667000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127041.3127061"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,29]]},"references-count":36,"alternative-id":["10.1145\/3127041.3127061","10.1145\/3127041"],"URL":"https:\/\/doi.org\/10.1145\/3127041.3127061","relation":{},"subject":[],"published":{"date-parts":[[2017,9,29]]},"assertion":[{"value":"2017-09-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}