Verifying an HTTP Key-Value Server with Interaction Trees and VST

Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li 0004, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In Liron Cohen 0001, Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). Volume 193 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. [doi]

@inproceedings{ZhangHK0LXBMPZ21,
  title = {Verifying an HTTP Key-Value Server with Interaction Trees and VST},
  author = {Hengchu Zhang and Wolf Honoré and Nicolas Koh and Yao Li 0004 and Yishuai Li and Li-yao Xia and Lennart Beringer and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
  year = {2021},
  doi = {10.4230/LIPIcs.ITP.2021.32},
  url = {https://doi.org/10.4230/LIPIcs.ITP.2021.32},
  researchr = {https://researchr.org/publication/ZhangHK0LXBMPZ21},
  cites = {0},
  citedby = {0},
  booktitle = {12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  editor = {Liron Cohen 0001 and Cezary Kaliszyk},
  volume = {193},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  isbn = {978-3-95977-188-7},
}