I. Alberdi, P. Owezarski, and V. Nicomette, Luth: Composing and Parallelizing Midpoint Inspection Devices, 2010 Fourth International Conference on Network and System Security, pp.9-16, 2010.
DOI : 10.1109/NSS.2010.44

M. Barnett, K. R. Leino, S. Mccanne, and S. L. Graham, Weakest-precondition of unstructured programs Bpf+: exploiting global data-flow optimization in a generalized packet filter architecture, PASTE '05: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering: SIGCOMM '99: Proceedings of the conference on Applications, technologies, architectures, and protocols for computer communication, pp.82-87, 1999.

N. Borisov, D. Brumley, H. J. Wang, J. Dunagan, P. Joshi et al., Generic application-level protocol analyzer and its language, p.NDSS, 2007.

H. Bos, W. De-bruijn, M. Cristea, T. Nguyen, and G. Portokalidis, FFPF: Fairly Fast Packet Filters, OSDI'04: Proceedings of the 6th conference on Symposium on Opearting Systems Design and Implementation, 2004.

A. Chlipala, Certified Programming with Dependent Types. Online in-progress textbook, 2009.

D. Chu, L. Popa, A. Tavakoli, J. Hellerstein, P. Levis et al., The design and implementation of a declarative sensor network system, Proceedings of the 5th international conference on Embedded networked sensor systems , SenSys '07, 2007.
DOI : 10.1145/1322263.1322281

S. Conchon, E. Contejean, J. Kanig, and S. Lescuyer, Lightweight integration of the Ergo theorem prover inside a proof assistant, Proceedings of the second workshop on Automated formal methods , AFM '07, pp.55-59, 2007.
DOI : 10.1145/1345169.1345176

J. C. Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of functional Programming, vol.13, issue.4, pp.709-745, 2003.
DOI : 10.1017/S095679680200446X

J. Filliâtre, Why: A Multi-Language Multi-Prover Verification Tool, Research Report, vol.1366, 2003.

M. Frigo, A fast Fourier transform compiler, ACM SIGPLAN Notices, vol.34, issue.5, 1999.
DOI : 10.1145/301631.301661
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.129.7986

X. Leroy, Mechanized semantics In: Logics and languages for reliability and security , NATO Science for Peace and Security Series D: Information and Communication Security, pp.195-224

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

A. Madhavapeddy, Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language, International Conference on Formal Engineering Methods, 2009.
DOI : 10.1007/978-3-642-10373-5_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.157.5372

A. Madhavapeddy, A. Ho, T. Deegan, D. Scott, and R. Sohan, Melange: Towards a functional Internet, Proceedings of the 2nd ACM SIGOPS/EuroSys European Conference on Computer Systems, 2007.

B. Pagano, O. Andrieu, T. Moniot, B. Canou, E. Chailloux et al., Experience report: using Objective Caml to develop safety-critical embedded tools in a certification framework, ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming, pp.215-220, 2009.

R. Pang, V. Paxson, R. Sommer, and L. Peterson, binpac, Proceedings of the 6th ACM SIGCOMM on Internet measurement , IMC '06, pp.289-300, 2006.
DOI : 10.1145/1177080.1177119

S. Institute, Top 20 internet security problems, threats and risks. section 5 anti-virus software Snort Team: Snort Users Manual. The official documentation produced by the Snort team at Sourcefire, 2007.