{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:24Z","timestamp":1772163984474,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,1,26]],"date-time":"2011-01-26T00:00:00Z","timestamp":1296000000000},"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":[[2011,1,26]]},"DOI":"10.1145\/1926385.1926387","type":"proceedings-article","created":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T09:58:22Z","timestamp":1295863102000},"page":"1-2","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Verified squared"],"prefix":"10.1145","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[{"name":"INRIA Paris-Rocquencourt, Le Chesnay, France"}]}],"member":"320","published-online":{"date-parts":[[2011,1,26]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_2_2_2_1","volume-title":"20th Int. Conf. TPHOLs 2007","volume":"4732","author":"Appel A. W.","year":"2007","unstructured":"A. W. Appel and S. Blazy . Separation logic for small-step Cminor. In Theorem Proving in Higher Order Logics , 20th Int. Conf. TPHOLs 2007 , volume 4732 of Lecture Notes in Computer Science LNCS, pages 5--21. Springer , 2007 . A. W. Appel and S. Blazy. Separation logic for small-step Cminor. In Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science LNCS, pages 5--21. Springer, 2007."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538917.1538919"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_8"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02614-0_10"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_2_9_1","volume-title":"CrossTalk","author":"Kornecki A. J.","year":"2006","unstructured":"A. J. Kornecki and J. Zalewski . The qualification of software development tools from the DO-178B certification perspective . CrossTalk , Apr. 2006 . A. J. Kornecki and J. Zalewski. The qualification of software development tools from the DO-178B certification perspective. CrossTalk, Apr. 2006."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/646482.691453"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053469"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_34"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542512"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"}],"event":{"name":"POPL '11: The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Austin Texas USA","acronym":"POPL '11","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1926385.1926387","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1926385.1926387","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:59:51Z","timestamp":1750229991000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1926385.1926387"}},"subtitle":["does critical software deserve verified tools?"],"short-title":[],"issued":{"date-parts":[[2011,1,26]]},"references-count":18,"alternative-id":["10.1145\/1926385.1926387","10.1145\/1926385"],"URL":"https:\/\/doi.org\/10.1145\/1926385.1926387","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1925844.1926387","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2011,1,26]]},"assertion":[{"value":"2011-01-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}