# From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server

arXiv: https://arxiv.org/abs/1811.11911 · HTML: https://mlsanity.com/paper/1811.11911/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Nov 2018.

## Built on by (most cited first, 1 of 1)

- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)

## Abstract (arXiv)

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.