{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:38Z","timestamp":1772164058007,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":96,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1553471 and 1564207"],"award-info":[{"award-number":["1553471 and 1564207"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009867","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"859-873","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["LMS-Verify: abstraction without regret for verified systems programming"],"prefix":"10.1145","author":[{"given":"Nada","family":"Amin","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tiark","family":"Rompf","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102165"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1944862.1944865"},{"key":"e_1_3_2_1_4_1","volume-title":"PolarSSL security advisory 2014-04","year":"2015","unstructured":"ARMmbed. PolarSSL security advisory 2014-04, 2015."},{"key":"e_1_3_2_1_5_1","unstructured":"https: \/\/tls.mbed.org\/tech-updates\/security-advisories\/polarsslsecurity-advisory-2014-04."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_2_1_8_1","volume-title":"ACSL: ANSI\/ISO C Specification Language, reference manual, version 1.11","author":"Baudin P.","year":"2009","unstructured":"P. Baudin, P. Cuoq, J.-C. Filli\u00e2tre, C. March\u00e9, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI\/ISO C Specification Language, reference manual, version 1.11, 2009-2016. http:\/\/frama-c.com\/download\/acsl.pdf."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784740"},{"key":"e_1_3_2_1_10_1","first-page":"306","volume-title":"Domain-Specific Program Generation","author":"Beckmann O.","year":"2003","unstructured":"O. Beckmann, A. Houghton, M. R. Mellor, and P. H. J. Kelly. Runtime code generation in C++ as a foundation for domain-specific optimisation. In Domain-Specific Program Generation, pages 291\u2013306, 2003."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032320"},{"key":"e_1_3_2_1_12_1","volume-title":"29th European Conference on Object-Oriented Programming, ECOOP 2015","volume":"37","author":"Boyland J. T.","year":"2015","unstructured":"J. T. Boyland, editor. 29th European Conference on Object-Oriented Programming, ECOOP 2015, July 5-10, 2015, Prague, Czech Republic, volume 37 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015."},{"issue":"4","key":"e_1_3_2_1_13_1","first-page":"4","article-title":"The bugs we have to kill. ; login:: the magazine of USENIX &","volume":"40","author":"Bratus S.","year":"2015","unstructured":"S. Bratus, M. L. Patterson, and A. Shubina. The bugs we have to kill. ; login:: the magazine of USENIX & SAGE, 40(4):4\u201310, 2015.","journal-title":"SAGE"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2011.15"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/954186.954190"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677003"},{"key":"e_1_3_2_1_20_1","unstructured":"U. Costa. Correct sorting with Frama-C and some thoughts on formal methdos Feb 2011. ulissesaraujo.wordpress.com."},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"30","volume-title":"ESOP","author":"Cousot P.","unstructured":"P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min\u00e9, D. Monniaux, and X. Rival. The astre\u00e9 analyzer. In ESOP, volume 3444 of Lecture Notes in Computer Science, pages 21\u201330. Springer, 2005."},{"key":"e_1_3_2_1_22_1","volume-title":"Springer Berlin Heidelberg","author":"Cuoq P.","year":"2012","unstructured":"P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C, pages 233\u2013247. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_12"},{"key":"e_1_3_2_1_24_1","unstructured":"CVE. 2002-0392: Apache security advisory. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2002- 0392."},{"key":"e_1_3_2_1_25_1","volume-title":"2013-2028: nginx security advisory. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2013-","author":"CVE.","year":"2028","unstructured":"CVE. 2013-2028: nginx security advisory. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2013- 2028."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2039346.2039348"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004574"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804318"},{"key":"e_1_3_2_1_30_1","first-page":"128","volume-title":"SNAPL 2015, May 3-6","volume":"32","author":"Felleisen M.","year":"2015","unstructured":"M. Felleisen, R. B. Findler, M. Flatt, S. Krishnamurthi, E. Barzilay, J. A. McCarthy, and S. Tobin-Hochstadt. The racket manifesto. In T. Ball, R. Bod\u00edk, S. Krishnamurthi, B. S. Lerner, and G. Morrisett, editors, 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA, volume 32 of LIPIcs, pages 113\u2013128. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_3_2_1_32_1","unstructured":"pages 48\u201359. ACM 2002."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2402676.2402695"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1508293.1508305"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301661"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010043619517"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCA.2011.6137940"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_4"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628146"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449913.1449935"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986314"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/647699.734160"},{"key":"e_1_3_2_1_44_1","volume-title":"Sep","author":"Jonnalagedda M.","year":"2015","unstructured":"M. Jonnalagedda. Staged parser combinators and recursion, Sep 2015. manojo.github.io."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660241"},{"key":"e_1_3_2_1_46_1","first-page":"51","volume-title":"Boyland {11}","author":"Keil M.","unstructured":"M. Keil and P. Thiemann. Treatjs: Higher-order contracts for javascripts. In Boyland {11}, pages 28\u201351."},{"key":"e_1_3_2_1_47_1","volume-title":"Beautiful Code","author":"Kernighan B.","year":"2007","unstructured":"B. Kernighan and R. Pike. A regular expression matcher. In G. Wilson and A. Oram, editors, Beautiful Code, chapter 1. O\u2019Reilly, 2007."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.14778\/2732951.2732959"},{"key":"e_1_3_2_1_50_1","series-title":"Lecture Notes in Computer Science","first-page":"15","volume-title":"NFM","author":"Kuncak V.","unstructured":"V. Kuncak. Developing verified software using leon. In NFM, volume 9058 of Lecture Notes in Computer Science, pages 12\u201315. Springer, 2015."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1787234.1787253"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2011.68"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/331960.331977"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(88)90022-2"},{"key":"e_1_3_2_1_58_1","series-title":"Lecture Notes in Computer Science","first-page":"307","volume-title":"VSTTE","author":"Meyer B.","unstructured":"B. Meyer. Eiffel as a framework for verification. In VSTTE, volume 4171 of Lecture Notes in Computer Science, pages 301\u2013307. Springer, 2005."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_3_2_1_61_1","volume-title":"Higher-order symbolic execution for contract verification and refutation","author":"Nguyen P. C.","year":"2015","unstructured":"P. C. Nguyen, S. Tobin-Hochstadt, and D. V. Horn. Higher-order symbolic execution for contract verification and refutation. 2015."},{"key":"e_1_3_2_1_62_1","unstructured":"nodejs & nginx. HTTP parser. https:\/\/github.com\/nodejs\/http-parser."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517208.2517228"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541568.2541570"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1177\/1094342004041291"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185520.2185528"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462176"},{"key":"e_1_3_2_1_68_1","unstructured":"J. Regehr. Comments on a formal verification of PolarSSL 2015. http:\/\/blog.regehr.org\/archives\/1261."},{"key":"e_1_3_2_1_69_1","volume-title":"User-defined types and procedural data structures as complementary approaches to data abstraction","author":"Reynolds J.","year":"1975","unstructured":"J. Reynolds. User-defined types and procedural data structures as complementary approaches to data abstraction. 1975."},{"key":"e_1_3_2_1_70_1","series-title":"Lecture Notes in Computer Science","first-page":"340","volume-title":"ITP","author":"Rizkallah C.","unstructured":"C. Rizkallah, J. Lim, Y. Nagashima, T. Sewell, Z. Chen, L. O\u2019Connor, T. C. Murray, G. Keller, and G. Klein. A framework for the automatic formal verification of refinement from cogent to C. In ITP, volume 9807 of Lecture Notes in Computer Science, pages 323\u2013340. Springer, 2016."},{"key":"e_1_3_2_1_71_1","unstructured":"T. Rompf. Lightweight Modular Staging and Embedded Compilers: Abstraction Without Regret for High-Level High-Performance Programming. PhD thesis EPFL 2012."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","unstructured":"T. Rompf N. Amin A. Moors P. Haller and M. Odersky. Scalavirtualized: Linguistic reuse for deep embeddings. Higher-Order and Symbolic Computation (Special issue for PEPM\u201912). 10.1007\/s10990-013-9096-9","DOI":"10.1007\/s10990-013-9096-9"},{"key":"e_1_3_2_1_73_1","volume-title":"SNAPL","author":"Rompf T.","year":"2015","unstructured":"T. Rompf, K. J. Brown, H. Lee, A. K. Sujeeth, M. Jonnalagedda, N. Amin, G. Ofenbeck, A. Stojanov, Y. Klonatos, M. Dashti, C. Koch, M. P\u00fcschel, and K. Olukotun. Go meta! A case for generative programming and dsls in performance critical systems. In SNAPL, 2015."},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2184319.2184345"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429128"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.66.5"},{"key":"e_1_3_2_1_77_1","unstructured":"Scala-LMS. Tutorial: Automata-based regex matcher. http:\/\/scala-lms.github.io\/tutorials\/automata.html."},{"key":"e_1_3_2_1_78_1","unstructured":"Scala-LMS. Tutorial: From interpreter to compiler. http:\/\/scala-lms.github.io\/tutorials\/regex.html."},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633632"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010000313106"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/2518189"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384685"},{"key":"e_1_3_2_1_83_1","volume-title":"Proceedings of the 28th International Conference on Machine Learning, ICML","author":"Sujeeth A. K.","year":"2011","unstructured":"A. K. Sujeeth, H. Lee, K. J. Brown, T. Rompf, M. Wu, A. R. Atreya, M. Odersky, and K. Olukotun. OptiML: an implicitly parallel domainspecific language for machine learning. In Proceedings of the 28th International Conference on Machine Learning, ICML, 2011."},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_3"},{"key":"e_1_3_2_1_85_1","volume-title":"TFP","author":"Svenningsson J.","year":"2012","unstructured":"J. Svenningsson and E. Axelsson. Combining deep and shallow embedding for EDSL. In TFP, 2012."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.13"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_3_2_1_88_1","first-page":"27","volume-title":"Boyland {11}","author":"Takikawa A.","unstructured":"A. Takikawa, D. Feltey, E. Dean, M. Flatt, R. B. Findler, S. Tobin-Hochstadt, and M. Felleisen. Towards practical gradual typing. In Boyland {11}, pages 4\u201327."},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837630"},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_3_2_1_91_1","unstructured":"TrustInSoft. PolarSSL 1.1.8 verification kit 2015. http:\/\/trust-in-soft.com\/polarSSL_demo.pdf."},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685052"},{"key":"e_1_3_2_1_94_1","doi-asserted-by":"crossref","unstructured":"pages 33\u201347. USENIX Association 2014.","DOI":"10.3917\/sigila.033.0047"},{"key":"e_1_3_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-8191(00)00087-9"},{"key":"e_1_3_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043197"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009867","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009867","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009867","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:43:03Z","timestamp":1763458983000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009867"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":96,"alternative-id":["10.1145\/3009837.3009867","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009867","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009867","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}