The purpose of this webpage is to provide the Coq formalization discussed in:
- Reynald Affeldt and Kazuhiko Sakaguchi.
An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing.
Journal of Formalized Reasoning, 7(1):63-104, 2014. pdf
Reynald Affeldt and Nicolas Marti.
Towards Formal Verification of TLS Network Packet Processing Written in C.
In 7th ACM SIGPLAN Workshop on Programming Languages meets Program Verification
(PLPV 2013), January 22, 2013, Rome, Italy, pages 35-46. ACM, January 2013.
coqdoc-generated documentation (look at "seplogC").
A more succint documentation focusing on lemmas and tactics used in our case-study:
Overview of the seplogC Library.
Draft. Last update: April 23, 2014.
Formalization as of 2017/01/06
- Requirements: MathComp-1.6.1 and
- Installation: see the file
SEPLOGCINSTALL in the root directory.