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.

李弈帅，2016年毕业于中国科学技术大学少年班学院，现就读于宾夕法尼亚大学计算机与信息科学系，参与美国自然科学基金会“Deep Specification”项目。研究方向：程序语言、软件测试与验证。