1. From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
- Author
-
Yao Li, Yishuai Li, Li-yao Xia, William Mansky, Benjamin C. Pierce, Nicolas Koh, Wolf Honoré, Lennart Beringer, and Steve Zdancewic
- Subjects
Structure (mathematical logic) ,FOS: Computer and information sciences ,Computer Science - Programming Languages ,Programming language ,Computer science ,Semantics (computer science) ,020207 software engineering ,0102 computer and information sciences ,02 engineering and technology ,computer.software_genre ,01 natural sciences ,010201 computation theory & mathematics ,0202 electrical engineering, electronic engineering, information engineering ,computer ,Formal verification ,Programming Languages (cs.PL) - 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., 13 pages + references
- Published
- 2018