{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:17:00Z","timestamp":1784233020960,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":50,"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"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1521602,1521539,1521523,1005849"],"award-info":[{"award-number":["1521602,1521539,1521523,1005849"]}],"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":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294106","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"234-248","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":39,"title":["From C to interaction trees: specifying, verifying, and testing a networked server"],"prefix":"10.1145","author":[{"given":"Nicolas","family":"Koh","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yao","family":"Li","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yishuai","family":"Li","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Li-yao","family":"Xia","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lennart","family":"Beringer","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wolf","family":"Honor\u00e9","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"William","family":"Mansky","sequence":"additional","affiliation":[{"name":"University of Illinois at Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"The Third International Workshop on Coq for Programming Languages (CoqPL).","author":"Anand Abhishek","year":"2017","unstructured":"Abhishek Anand , Andrew Appel , Greg Morrisett , Zoe Paraskevopoulou , Randy Pollack , Olivier Savary Belanger , Matthieu Sozeau , and Matthew Weaver . 2017 . CertiCoq: A verified compiler for Coq . In The Third International Workshop on Coq for Programming Languages (CoqPL). Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In The Third International Workshop on Coq for Programming Languages (CoqPL)."},{"key":"e_1_3_2_1_2_1","volume-title":"Program Logics - for Certified Compilers","author":"Appel Andrew W.","unstructured":"Andrew W. Appel . 2014. Program Logics - for Certified Compilers . Cambridge University Press . http:\/\/www.cambridge.org\/de\/academic\/subjects\/ computer-science\/programming-languages-and-applied-logic\/ program-logics-certified-compilers?format=HB Andrew W. Appel. 2014. Program Logics - for Certified Compilers. Cambridge University Press. http:\/\/www.cambridge.org\/de\/academic\/subjects\/ computer-science\/programming-languages-and-applied-logic\/ program-logics-certified-compilers?format=HB"},{"key":"e_1_3_2_1_3_1","article-title":"Position paper: the science of deep specification","volume":"375","author":"Appel Andrew W.","year":"2017","unstructured":"Andrew W. Appel , Lennart Beringer , Adam Chlipala , Benjamin C. Pierce , Zhong Shao , Stephanie Weirich , and Steve Zdancewic . 2017 . Position paper: the science of deep specification . Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences 375 , 2104 (2017). Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. 2017. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences 375, 2104 (2017).","journal-title":"Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2015.7107466"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"M. Belshe R. Peon and M. Thomson. 2015. Hypertext Transfer Protocol Version 2 (HTTP\/2). RFC 7540. RFC Editor. http:\/\/www.rfc-editor.org\/ rfc\/rfc7540.txt  M. Belshe R. Peon and M. Thomson. 2015. Hypertext Transfer Protocol Version 2 (HTTP\/2). RFC 7540. RFC Editor. http:\/\/www.rfc-editor.org\/ rfc\/rfc7540.txt","DOI":"10.17487\/RFC7540"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806634"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_1_13_1","volume-title":"13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18)","author":"Chajed Tej","year":"2018","unstructured":"Tej Chajed , Frans Kaashoek , Butler Lampson , and Nickolai Zeldovich . 2018 . Verifying a concurrent mail server with CSPEC . In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18) . USENIX Association, Carlsbad, CA. https:\/\/www.usenix.org\/conference\/osdi18\/ presentation\/chajed Tej Chajed, Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich. 2018. Verifying a concurrent mail server with CSPEC. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18). USENIX Association, Carlsbad, CA. https:\/\/www.usenix.org\/conference\/osdi18\/ presentation\/chajed"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677003"},{"key":"e_1_3_2_1_15_1","volume-title":"Certified Programming with Dependent Types","author":"Chlipala Adam","unstructured":"Adam Chlipala . 2017. Infinite Data and Proofs . In Certified Programming with Dependent Types . MIT Press . http:\/\/adam.chlipala.net\/cpdt\/html\/ Cpdt.Coinductive.html Adam Chlipala. 2017. Infinite Data and Proofs. In Certified Programming with Dependent Types. MIT Press. http:\/\/adam.chlipala.net\/cpdt\/html\/ Cpdt.Coinductive.html"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/C-M.1978.218136"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03592-1_6"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_19"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_21_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan (Newman) Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016 , Savannah, GA, USA , November 2-4, 2016. 653\u2013669. https:\/\/www.usenix. org\/conference\/osdi16\/technical-sessions\/presentation\/gu Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016. 653\u2013669. https:\/\/www.usenix. org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_25_1","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel , Jon Howell , Jacob R. Lorch , Arjun Narayan , Bryan Parno , Danfeng Zhang , and Brian Zill . 2014 . Ironclad Apps: End-to-End Security via Automated Full-System Verification . In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914 , Broomfield, CO, USA , October 6-8, 2014. 165\u2013181. https:\/\/www.usenix.org\/conference\/ osdi14\/technical-sessions\/presentation\/hawblitzel Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914, Broomfield, CO, USA, October 6-8, 2014. 165\u2013181. https:\/\/www.usenix.org\/conference\/ osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_3_2_1_26_1","volume-title":"European Symposium on Programming, Saarbr\u00fccken, Federal Republic of Germany","author":"He Jifeng","year":"1986","unstructured":"Jifeng He , C. A. R. Hoare , and Jeff W. Sanders . 1986. Data Refinement Refined. In ESOP 86 , European Symposium on Programming, Saarbr\u00fccken, Federal Republic of Germany , March 17-19, 1986 , Proceedings. 187\u2013196. Jifeng He, C. A. R. Hoare, and Jeff W. Sanders. 1986. Data Refinement Refined. In ESOP 86, European Symposium on Programming, Saarbr\u00fccken, Federal Republic of Germany, March 17-19, 1986, Proceedings. 187\u2013196."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2016.37"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034654.2034667"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_3_2_1_32_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley . Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_3_2_1_33_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2018","unstructured":"Leonidas Lampropoulos and Benjamin C . Pierce . 2018 . QuickChick: Property Based Testing in Coq. Electronic textbook. https:\/\/softwarefoundations. cis.upenn.edu\/qc-current\/index.html Leonidas Lampropoulos and Benjamin C. Pierce. 2018. QuickChick: PropertyBased Testing in Coq. Electronic textbook. https:\/\/softwarefoundations. cis.upenn.edu\/qc-current\/index.html"},{"key":"e_1_3_2_1_34_1","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming Artificial Intelligence and Reasoning - 16th International Conference LPAR-16 Dakar Senegal April 25-May 1 2010 Revised Selected Papers. 348\u2013370.   K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming Artificial Intelligence and Reasoning - 16th International Conference LPAR-16 Dakar Senegal April 25-May 1 2010 Revised Selected Papers. 348\u2013370."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_36_1","volume-title":"FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings. 338\u2013354","author":"Letan Thomas","year":"2018","unstructured":"Thomas Letan , Yann R\u00e9gis-Gianas , Pierre Chifflier , and Guillaume Hiet . 2018 . Modular Verification of Programs with Effects and Effect Handlers in Coq. In Formal Methods - 22nd International Symposium , FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings. 338\u2013354 . Thomas Letan, Yann R\u00e9gis-Gianas, Pierre Chifflier, and Guillaume Hiet. 2018. Modular Verification of Programs with Effects and Effect Handlers in Coq. In Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings. 338\u2013354."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.08.004"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133911"},{"key":"e_1_3_2_1_40_1","unstructured":"Coq development team. 2017. Coq and Axioms. https:\/\/github.com\/coq\/ coq\/wiki\/CoqAndAxioms  Coq development team. 2017. Coq and Axioms. https:\/\/github.com\/coq\/ coq\/wiki\/CoqAndAxioms"},{"key":"e_1_3_2_1_41_1","unstructured":"Coq development team. 2018. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.8.1.  Coq development team. 2018. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.8.1."},{"key":"e_1_3_2_1_42_1","volume-title":"MPC 2015, K\u00f6nigswinter, Germany, June 29 - July 1, 2015. Proceedings. 257\u2013275","author":"McBride Conor","year":"2015","unstructured":"Conor McBride . 2015 . Turing-Completeness Totally Free. In Mathematics of Program Construction - 12th International Conference , MPC 2015, K\u00f6nigswinter, Germany, June 29 - July 1, 2015. Proceedings. 257\u2013275 . Conor McBride. 2015. Turing-Completeness Totally Free. In Mathematics of Program Construction - 12th International Conference, MPC 2015, K\u00f6nigswinter, Germany, June 29 - July 1, 2015. Proceedings. 257\u2013275."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_44_1","volume-title":"Proceedings of the 1999 USENIX Annual Technical Conference","author":"Pai Vivek S.","year":"1999","unstructured":"Vivek S. Pai , Peter Druschel , and Willy Zwaenepoel . 1999 . Flash: An efficient and portable Web server . In Proceedings of the 1999 USENIX Annual Technical Conference , June 6-11, 1999, Monterey, California, USA. 199\u2013212. http:\/\/www.usenix.org\/events\/usenix99\/full_papers\/pai\/pai.pdf Vivek S. Pai, Peter Druschel, and Willy Zwaenepoel. 1999. Flash: An efficient and portable Web server. In Proceedings of the 1999 USENIX Annual Technical Conference, June 6-11, 1999, Monterey, California, USA. 199\u2013212. http:\/\/www.usenix.org\/events\/usenix99\/full_papers\/pai\/pai.pdf"},{"key":"e_1_3_2_1_45_1","volume-title":"ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 158\u2013182","author":"Penninckx Willem","year":"2015","unstructured":"Willem Penninckx , Bart Jacobs , and Frank Piessens . 2015 . Sound, Modular and Compositional Verification of the Input\/Output Behavior of Programs. In Programming Languages and Systems - 24th European Symposium on Programming , ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 158\u2013182 . Willem Penninckx, Bart Jacobs, and Frank Piessens. 2015. Sound, Modular and Compositional Verification of the Input\/Output Behavior of Programs. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 158\u2013182."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480934"},{"key":"e_1_3_2_1_49_1","volume-title":"Minimizing Faulty Executions of Distributed Systems. In 13th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2016","author":"Scott Colin","year":"2016","unstructured":"Colin Scott , Aurojit Panda , Vjekoslav Brajkovic , George C. Necula , Arvind Krishnamurthy , and Scott Shenker . 2016 . Minimizing Faulty Executions of Distributed Systems. In 13th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2016 , Santa Clara, CA, USA , March 16-18, 2016. 291\u2013309. https:\/\/www.usenix.org\/conference\/nsdi16\/ technical-sessions\/presentation\/scott Colin Scott, Aurojit Panda, Vjekoslav Brajkovic, George C. Necula, Arvind Krishnamurthy, and Scott Shenker. 2016. Minimizing Faulty Executions of Distributed Systems. In 13th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2016, Santa Clara, CA, USA, March 16-18, 2016. 291\u2013309. https:\/\/www.usenix.org\/conference\/nsdi16\/ technical-sessions\/presentation\/scott"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048073"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02652-2_21"},{"key":"e_1_3_2_1_53_1","volume-title":"Proceedings of the NATO Advanced Study Institute on Program Design Calculi","author":"Wadler Philip","year":"1992","unstructured":"Philip Wadler . 1992 . Monads for functional programming. In Program Design Calculi , Proceedings of the NATO Advanced Study Institute on Program Design Calculi , Marktoberdorf, Germany, July 28 - August 9, 1992. 233\u2013264. Philip Wadler. 1992. Monads for functional programming. In Program Design Calculi, Proceedings of the NATO Advanced Study Institute on Program Design Calculi, Marktoberdorf, Germany, July 28 - August 9, 1992. 233\u2013264."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Cascais Portugal","acronym":"CPP '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"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.3294106","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294106","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294106","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.3294106"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":50,"alternative-id":["10.1145\/3293880.3294106","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294106","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"}}]}}