{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:59:27Z","timestamp":1755838767858,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"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":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294105","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"222-233","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["A verified protocol buffer compiler"],"prefix":"10.1145","author":[{"given":"Qianchuan","family":"Ye","sequence":"first","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Delaware","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2016. CVE-2016-5080. Available from MITRE CVE-ID CVE-2016-5080.. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2016-5080  2016. CVE-2016-5080. Available from MITRE CVE-ID CVE-2016-5080.. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2016-5080"},{"key":"e_1_3_2_1_2_1","unstructured":"2017. CVE-2017-9023. Available from MITRE CVE-ID CVE-2017-9023.. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2017-9023  2017. CVE-2017-9023. Available from MITRE CVE-ID CVE-2017-9023.. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2017-9023"},{"key":"e_1_3_2_1_3_1","unstructured":"2018. CVE-2018-11058. Available from MITRE CVE-ID CVE-2018-11058.. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name= CVE-2018-11058  2018. CVE-2018-11058. Available from MITRE CVE-ID CVE-2018-11058.. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name= CVE-2018-11058"},{"key":"e_1_3_2_1_4_1","volume-title":"http:\/\/avro.apache.org\/docs\/current\/ {Accessed","author":"Foundation Apache Software","year":"2016","unstructured":"Apache Software Foundation . 2016. Apache Avro 1.8.0 Documentation . http:\/\/avro.apache.org\/docs\/current\/ {Accessed May 04, 2016 }. Apache Software Foundation. 2016. Apache Avro 1.8.0 Documentation. http:\/\/avro.apache.org\/docs\/current\/ {Accessed May 04, 2016}."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_12"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Tim Bray. 2017. The JavaScript Object Notation (JSON) Data Interchange Format. RFC 8259.  Tim Bray. 2017. The JavaScript Object Notation (JSON) Data Interchange Format. RFC 8259.","DOI":"10.17487\/RFC8259"},{"key":"e_1_3_2_1_7_1","first-page":"27","article-title":"Extensible Markup Language (XML)","volume":"2","author":"Bray Tim","year":"1997","unstructured":"Tim Bray , Jean Paoli , C Michael Sperberg-McQueen , Eve Maler , and Fran\u00e7ois Yergeau . 1997 . Extensible Markup Language (XML) . World Wide Web Journal 2 , 4 (1997), 27 \u2013 66 . Tim Bray, Jean Paoli, C Michael Sperberg-McQueen, Eve Maler, and Fran\u00e7ois Yergeau. 1997. Extensible Markup Language (XML). World Wide Web Journal 2, 4 (1997), 27\u201366.","journal-title":"World Wide Web Journal"},{"volume-title":"Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant","author":"Chlipala Adam","key":"e_1_3_2_1_8_1","unstructured":"Adam Chlipala . 2013. Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant . MIT Press . Adam Chlipala. 2013. Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant. MIT Press."},{"key":"e_1_3_2_1_9_1","unstructured":"Nathan Collins Mark Tullsen Aaron Tomb and Lee Pike. 2017. Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System. In Embedded Security in Cars (ESCARS).  Nathan Collins Mark Tullsen Aaron Tomb and Lee Pike. 2017. Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System. In Embedded Security in Cars (ESCARS)."},{"key":"e_1_3_2_1_10_1","volume-title":"d.}. NARCISSUS: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. arXiv","author":"Delaware Benjamin","year":"1803","unstructured":"Benjamin Delaware , Sorawit Suriyakarn , Cl\u00e9ment Pit-Claudel , Qianchuan Ye , and Adam Chlipala . {n. d.}. NARCISSUS: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. arXiv : 1803 .04870 Benjamin Delaware, Sorawit Suriyakarn, Cl\u00e9ment Pit-Claudel, Qianchuan Ye, and Adam Chlipala. {n. d.}. NARCISSUS: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. arXiv: 1803.04870"},{"volume-title":"Constructing Semantic Models of Programs with the Software Analysis Workbench","author":"Dockins Robert","key":"e_1_3_2_1_11_1","unstructured":"Robert Dockins , Adam Foltzer , Joe Hendrix , Brian Huffman , Dylan McNamee , and Aaron Tomb . 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench . In Verified Software. Theories, Tools, and Experiments, Sandrine Blazy and Marsha Chechik (Eds.). Springer International Publishing , Cham , 56\u201372. Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee, and Aaron Tomb. 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench. In Verified Software. Theories, Tools, and Experiments, Sandrine Blazy and Marsha Chechik (Eds.). Springer International Publishing, Cham, 56\u201372."},{"key":"e_1_3_2_1_12_1","unstructured":"Olivier Dubuisson. 2001. ASN. 1: communication between heterogeneous systems. Morgan Kaufmann.   Olivier Dubuisson. 2001. ASN. 1: communication between heterogeneous systems. Morgan Kaufmann."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_3_2_1_14_1","unstructured":"Python Software Foundation. 2018. Pickle - Python object serialization. https:\/\/docs.python.org\/3\/library\/pickle.html  Python Software Foundation. 2018. Pickle - Python object serialization. https:\/\/docs.python.org\/3\/library\/pickle.html"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"e_1_3_2_1_16_1","volume-title":"TRX: A Formally Verified Parser Interpreter. Logical Methods in Computer Science 7, 2","author":"Koprowski Adam","year":"2011","unstructured":"Adam Koprowski and Henri Binsztok . 2011 . TRX: A Formally Verified Parser Interpreter. Logical Methods in Computer Science 7, 2 (2011). Adam Koprowski and Henri Binsztok. 2011. TRX: A Formally Verified Parser Interpreter. Logical Methods in Computer Science 7, 2 (2011)."},{"key":"e_1_3_2_1_17_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2018. The OCaml system release 4.07 Documentation and user\u2019s manual - Module Marshal. https:\/\/caml. inria.fr\/pub\/docs\/manual-ocaml\/libref\/Marshal.html  Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2018. The OCaml system release 4.07 Documentation and user\u2019s manual - Module Marshal. https:\/\/caml. inria.fr\/pub\/docs\/manual-ocaml\/libref\/Marshal.html"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1035"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254111"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Jon Postel. 1981. Internet Protocol. RFC 791.  Jon Postel. 1981. Internet Protocol. RFC 791.","DOI":"10.17487\/rfc0791"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Jon Postel. 1981. Transmission Control Protocol. RFC 793.  Jon Postel. 1981. Transmission Control Protocol. RFC 793.","DOI":"10.17487\/rfc0793"},{"key":"e_1_3_2_1_22_1","volume-title":"courses.cs.washington.edu\/courses\/cse599w\/16sp\/projects\/cheerios.pdf","author":"Simmons Keith","year":"2016","unstructured":"Keith Simmons . 2016. Cheerios. ( 2016 ). courses.cs.washington.edu\/courses\/cse599w\/16sp\/projects\/cheerios.pdf . Keith Simmons. 2016. Cheerios. (2016). courses.cs.washington.edu\/courses\/cse599w\/16sp\/projects\/cheerios.pdf."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1832"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9429-1"},{"key":"e_1_3_2_1_25_1","unstructured":"The Coq Development Team. 2018. The Coq proof assistant reference manual version 8.8.1. (2018).  The Coq Development Team. 2018. The Coq proof assistant reference manual version 8.8.1. (2018)."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122975.3122979"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Cascais Portugal","acronym":"CPP '19"},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294105","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294105","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:50Z","timestamp":1750207430000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":27,"alternative-id":["10.1145\/3293880.3294105","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294105","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}