Authors
Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, Steve Zdancewic
Publication date
2021
Conference
12th International Conference on Interactive Theorem Proving (ITP 2021)
Publisher
Schloss Dagstuhl-Leibniz-Zentrum für Informatik
Description
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.
Total citations
Scholar articles
H Zhang, W Honoré, N Koh, Y Li, Y Li, LY Xia… - The 12th Conference on Interactive Theorem Proving, 2021