@inproceedings{abb15b01ba964a87a452f2b9bb8e7bdd,
title = "From C to interaction trees: Specifying, verifying, and testing a networked server",
abstract = "We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward one client at a time style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.",
keywords = "formal verification, interaction trees, network refinement, QuickChick, TCP, testing, VST",
author = "Nicolas Koh and Yao Li and Yishuai Li and Xia, {Li Yao} and Lennart Beringer and Wolf Honor{\'e} and William Mansky and Pierce, {Benjamin C.} and Steve Zdancewic",
note = "Publisher Copyright: {\textcopyright} 2019 ACM.; 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 ; Conference date: 14-01-2019 Through 15-01-2019",
year = "2019",
month = jan,
day = "14",
doi = "10.1145/3293880.3294106",
language = "English (US)",
series = "CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019",
publisher = "Association for Computing Machinery, Inc",
pages = "234--248",
editor = "Assia Mahboubi",
booktitle = "CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019",
}