@inproceedings{a863192404114d63a678ca778ad29d73,
title = "Verifying an HTTP key-value server with interaction trees and VST",
abstract = "We present a networked key-value server, implemented in C and formally verified in Coq. The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and verified using interaction trees and the Verified Software Toolchain. The codebase includes a reusable and fully verified C string library that provides 17 standard POSIX string functions and 17 general purpose non-POSIX string functions. For the KVServer socket system calls, we establish a refinement relation between specifications at user-space level and at CertiKOS kernel-space level.",
keywords = "Coq, Deep specification, Formal verification, HTTP",
author = "Hengchu Zhang and Wolf Honor{\'e} and Nicolas Koh and Yao Li and Yishuai Li and Xia, {Li Yao} and Lennart Beringer and William Mansky and Benjamin Pierce and Steve Zdancewic",
note = "Publisher Copyright: {\textcopyright} Hengchu Zhang, Wolf Honor{\'e}, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic.; 12th International Conference on Interactive Theorem Proving, ITP 2021 ; Conference date: 29-06-2021 Through 01-07-2021",
year = "2021",
month = jun,
day = "1",
doi = "10.4230/LIPIcs.ITP.2021.32",
language = "English (US)",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Liron Cohen and Cezary Kaliszyk",
booktitle = "12th International Conference on Interactive Theorem Proving, ITP 2021",
address = "Germany",
}