D. Kaloper-mer?injak, H. Mehnert, A. Madhavapeddy, and P. Sewell, Not-Quite-So- Broken TLS : Lessons in Re-Engineering a Security Protocol Specification and Implementation, 24th USENIX Security Symposium (USENIX Security 15), pp.223-238

A. Kantee, Flexible Operating System Internals : The Design and Implementation of the Anykernel and Rump Kernels, 2012.

A. Kivity, Y. Kamay, D. Laor, U. Lublin, and A. Liguori, KVM : the Linux Virtual Machine Monitor, Proceedings of the 2007 Ottawa Linux Symposium (OLS'-07, 2007.

G. Klein, K. Elphinstone, G. Heiser-andronick, D. Cock, P. Derrin et al., seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp.207-220, 2009.
DOI : 10.1145/1629575.1629596

I. M. Leslie, D. Mcauley, R. Black, T. Roscoe, P. T. Barham et al., The design and implementation of an operating system to support distributed multimedia applications, IEEE Journal on Selected Areas in Communications, vol.14, issue.7, pp.1280-1297, 1996.
DOI : 10.1109/49.536480

A. Madhavapeddy, T. Leonard, M. Skjegstad, T. Gazagnaire, D. Sheets et al., Jitsu : Just-In-Time Summoning of Unikernels, 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pp.559-573, 2015.

A. Madhavapeddy, R. Mortier, C. Rotsos, D. Scott, B. Singh et al., Unikernels : Library Operating Systems for the Cloud, Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '13, pp.461-472, 2013.

J. Martins, M. Ahmed, C. Raiciu, V. Olteanu, M. Honda et al., ClickOS and the Art of Network Function Virtualization, Proceedings of the 11th USENIX Conference on Networked Systems Design and Implementation, NSDI'14, pp.459-473, 2014.

D. E. Porter, S. Boyd-wickizer, J. Howell, R. Olinsky, and G. C. Hunt, Rethinking the library OS from the top down, Proc. 16th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp.291-304, 2011.
DOI : 10.1145/1950365.1950399
URL : http://www.cse.unsw.edu.au/%7Ecs9242/current/papers/libraryos_asplos11.pdf

T. Ridge, A B-tree library for OCaml, OCaml Workshop 2017, 2017.

D. Scott, R. Sharp, T. Gazagnaire, and A. Madhavapeddy, Using functional programming within an industrial product group : perspectives and perceptions, Proc. 15th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp.87-92, 2010.
DOI : 10.1145/1932681.1863557

D. Williams and R. Koller, Unikernel Monitors : Extending Minimalism Outside of the Box, 8th USENIX Workshop on Hot Topics in Cloud Computing, 2016.

. F. References, J. Bobot, C. Filliâtre, G. Marché, A. Melquiond et al., The Why3 platform 0.81, 2013. Tutorial and Reference Manual

M. P. Bonacina, S. Graham-lengrand, and N. Shankar, Satisfiability Modulo Theories and Assignments, Proc. of the 26th Int. Conf. on Automated Deduction (CADE'17), volume 10395 of LNAI, 2017.
DOI : 10.1007/978-3-319-40970-2_16
URL : https://hal.archives-ouvertes.fr/hal-01615830

M. P. Bonacina, S. Graham-lengrand, N. M. Shankar-]-l, G. O. De-moura, and . Passmore, Proofs in conflict-driven theory combination [CDS] The CDSAT system. https://github.com/disteph/cdsat [CH03] J. Cheney and R. Hinze. First-class phantom types [Coq] The Coq Proof Assistant The strategy challenge in SMT solving, Proc. of the 7th Int. Conf. on Certified Programs and Proofs (CPP'18 Automated Reasoning and Mathematics -Essays in Memory of William W. McCune, pp.15-44, 2003.

. [. Graham-lengrand, Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture, Proc. of the 22nd Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), pp.149-156, 2013.
DOI : 10.1007/978-3-642-40537-2_14
URL : https://hal.archives-ouvertes.fr/hal-00906789

M. Gordon, R. Milner, C. Wadsworth, ]. R. Edinburgh-lcfmil79, H. Milner et al., [Isa] The Isabelle theorem prover LCF: A way of doing proofs with a machine Guarded recursive datatype constructors, Proc. of the the 8th Int. Symp. on Mathematical Foundations of Computer Science Proceedings of the Thirtieth SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp.146-159, 1979.

]. S. Bardin, M. Delahaye, R. David, N. Kosmatov, M. Papadakis et al., Sound and Quasi-Complete Detection of Infeasible Test Requirements, 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST), pp.1-10, 2015.
DOI : 10.1109/ICST.2015.7102607

M. Barnett, B. E. Chang, R. Deline, B. Jacobs, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, Proceedings of FMCO, number 4111 in LNCS, pp.364-387, 2005.
DOI : 10.1007/11804192_17
URL : http://research.microsoft.com/~leino/papers/krml160.pdf

M. Barnett and K. R. Leino, Weakest-precondition of unstructured programs, Proceedings of PASTE'05, pp.82-87, 2005.
DOI : 10.1145/1108768.1108813
URL : http://research.microsoft.com/~leino/papers/krml157.pdf

M. Barnett, K. R. Leino, and W. Schulte, The Spec# Programming System: An Overview, Proceedings of CASSIS, pp.49-69, 2004.
DOI : 10.1007/978-3-540-30569-9_3
URL : http://research.microsoft.com/~leino/papers/krml136.pdf

P. Baudin, J. C. Filliâtre, T. Hubert, C. Marché, B. Monate et al., ACSL: ANSI C Specification Language (preliminary design V1.2), preliminary edition, 2008.

S. Böhme and M. Moskal, Heaps and Data Structures: A Challenge for Automated Provers, Proceedigns of CADE-23, pp.177-191, 2011.
DOI : 10.1007/978-3-642-02959-2_10

D. Bühler, Structuring an Abstract Interpreter through Value and State Abstractions, 2017.

C. Calcagno, D. Distefano, P. O. Hearn, and H. Yang, Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic, SAS, pp.182-203, 2006.
DOI : 10.1007/11823230_13

B. Chang, X. Rival, and G. Necula, Shape Analysis with Structural Invariant Checkers, Proceedings of SAS, pp.384-401, 2007.
DOI : 10.1007/978-3-540-74061-2_24
URL : http://larsg.hautetfort.com/files/2007_228_007_RESU.pdf

S. Chatterjee, S. K. Lahiri, S. Qadeer, and Z. Rakamari?, A low-level memory model and an accompanying reachability predicate, International Journal on Software Tools for Technology Transfer, vol.20, issue.1, pp.105-116, 2009.
DOI : 10.1007/s10009-009-0098-1
URL : http://www.cs.ubc.ca/~zrakamar/publications/sttt2009-clqr.pdf

W. Chin, C. David, H. H. Nguyen, and S. Qin, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Science of Computer Programming, vol.77, issue.9, pp.1006-1036, 2012.
DOI : 10.1016/j.scico.2010.07.004

L. Correnson, Qed. Computing What Remains to Be Proved, Proceedings of NFM, pp.215-229, 2014.
DOI : 10.1007/978-3-319-06200-6_17

L. Correnson and F. Bobot, Exploring memory models with Frama-C/WP, 2017.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, Proceedings of CAV, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

C. Flanagan and J. B. Saxe, Avoiding exponential explosion, ACM SIGPLAN Notices, vol.36, issue.3, pp.193-205, 2001.
DOI : 10.1145/373243.360220

T. Hubert and C. Marché, Separation analysis for deductive verification, Proceedings of HAV, pp.81-93, 2007.

B. Jacobs and F. Piessens, The VeriFast program verifier, 2008.
DOI : 10.1007/978-3-642-17164-2_21
URL : https://lirias.kuleuven.be/bitstream/123456789/275140/1/aplas2010..

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective. Formal Asp, Comput, vol.27, issue.3, pp.573-609, 2015.
DOI : 10.1007/s00165-014-0326-7

K. R. Leino, Efficient weakest preconditions, Information Processing Letters, vol.93, issue.6, pp.281-288, 2005.
DOI : 10.1016/j.ipl.2004.10.015
URL : http://research.microsoft.com/pubs/70052/tr-2004-34.pdf

X. Leroy, A. W. Appel, S. Blazy, and G. Stewart, The CompCert Memory Model, Version 2, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00703441

X. Leroy and S. Blazy, Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, vol.17, issue.5???6, pp.1-31, 2008.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/inria-00289542

F. Mehta and T. Nipkow, Proving pointer programs in higher-order logic, Proceedings of CADE-19, pp.121-135, 2003.
DOI : 10.1007/978-3-540-45085-6_10
URL : http://www.in.tum.de/~nipkow/pubs/cade03.ps.gz

P. W. O-'hearn, J. C. Reynolds, and H. Yang, Local reasoning about programs that alter data structures, Proceedings of CSL, pp.1-19, 2001.

R. Piskac, T. Wies, and D. Zufferey, Automating Separation Logic with Trees and Data, Proceedings of CAV, pp.711-728, 2014.
DOI : 10.1007/978-3-319-08867-9_47

Z. Rakamaric and A. J. Hu, A Scalable Memory Model for Low-Level Code, Proceedings of VMCAI, pp.290-304, 2009.
DOI : 10.1145/1321631.1321719

P. Sotin, B. Jeannet, and X. , Concrete Memory Models for Shape Analysis, Electronic Notes in Theoretical Computer Science, vol.267, issue.1, pp.139-150, 2010.
DOI : 10.1016/j.entcs.2010.09.012
URL : https://hal.archives-ouvertes.fr/hal-00786330

W. Wang, C. Barrett, and T. Wies, Partitioned Memory Models for Program Analysis, Proceedings of VMCAI, pp.539-558, 2017.
DOI : 10.1145/301618.301647

A. Abel, B. Pientka, D. Thibodeau, and A. Setzer, Copatterns, ACM SIGPLAN Notices, vol.48, issue.1, pp.27-38, 2013.
DOI : 10.1145/1328438.1328482

J. Bernardy and P. Jansson, Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda, Logical Methods in Computer Science, vol.12, issue.2, 2016.
DOI : 10.2168/LMCS-12(2:6)2016

E. Brady, Idris, a general-purpose dependently typed programming language: Design and implementation, Journal of Functional Programming, vol.36, issue.05, pp.552-593, 2013.
DOI : 10.1017/S0956796803004829

A. Janusz and . Brzozowski, Derivatives of regular expressions, Journal of the ACM (JACM), vol.11, issue.4, pp.481-494, 1964.

G. Couprie, Nom, A Byte oriented, streaming, Zero copy, Parser Combinators Library in Rust, 2015 IEEE Security and Privacy Workshops, pp.142-148, 2015.
DOI : 10.1109/SPW.2015.31

N. Anders-danielsson, Total parser combinators, ACM SIGPLAN Notices, vol.45, issue.9, pp.285-296, 2010.
DOI : 10.1145/1932681.1863585

P. Hudak, Building domain-specific embedded languages, ACM Computing Surveys, vol.28, issue.4es, p.196, 1996.
DOI : 10.1145/242224.242477
URL : http://www.kestrel.edu:80/~jullig/rio97/position-papers/ACM-WS.ps

G. Hutton and E. Meijer, Monadic parsing in Haskell, Journal of Functional Programming, vol.8, issue.4, pp.437-444, 1998.
DOI : 10.1017/S0956796898003050

J. Jourdan, F. Pottier, and X. Leroy, Validating LR(1) Parsers, ESOP, pp.397-416, 2012.
DOI : 10.1007/978-3-642-28869-2_20
URL : https://hal.archives-ouvertes.fr/hal-01077321

D. Leijen, P. Martini, and A. Latter, Parsec documentation. https://hackage. haskell.org, 2017.

X. Leroy, The CompCert verified compiler. Documentation and user's manual, INRIA Paris-Rocquencourt, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01399482

C. Mcbride and R. Paterson, Applicative programming with effects, Journal of Functional Programming, vol.18, issue.01, pp.1-13, 2008.
DOI : 10.1017/S0956796800003658

G. Berry, Stable models of typed lambda-calculi, In Int. Col. on Aut., Lang. and Programming LNCS, vol.62, pp.72-89, 1978.
DOI : 10.1007/3-540-08860-1_7

G. Berry and P. Curien, Sequential algorithms on concrete data structures, Theoretical Computer Science, vol.20, issue.3, pp.265-321, 1982.
DOI : 10.1016/S0304-3975(82)80002-9
URL : https://doi.org/10.1016/s0304-3975(82)80002-9

G. Berry and G. Gonthier, The Esterel synchronous programming language: design, semantics, implementation, Science of Computer Programming, vol.19, issue.2, pp.87-152, 1992.
DOI : 10.1016/0167-6423(92)90005-V
URL : https://hal.archives-ouvertes.fr/inria-00075711

P. Caspi and M. Pouzet, Synchronous Kahn networks, Int. Conf. Func. Prog. (ICFP), pp.226-238, 1996.
DOI : 10.1145/232629.232651
URL : http://www-spi.lip6.fr/lucid-synchrone/papers/sync_kahn.ps.gz

P. Caspi and M. Pouzet, A Co-iterative Characterization of Synchronous Stream Functions, Electronic Notes in Theoretical Computer Science, vol.11, pp.1-21, 1998.
DOI : 10.1016/S1571-0661(04)00050-7
URL : https://hal.archives-ouvertes.fr/hal-01622305

G. L. Cattani, I. Stark, and G. Winskel, Presheaf models for the ?-calculus, Category Theory and Computer Science (CTCT, 1997.

G. L. Cattani and G. Winskel, Presheaf models for CCS-like languages, Theoretical Computer Science, vol.300, issue.1-3, pp.47-89, 2003.
DOI : 10.1016/S0304-3975(01)00209-2
URL : https://doi.org/10.1016/s0304-3975(01)00209-2

J. Colaço, A. Girault, G. Hamon, and M. Pouzet, Towards a higher-order synchronous data-flow language, Proceedings of the fourth ACM international conference on Embedded software , EMSOFT '04, pp.230-239, 2004.
DOI : 10.1145/1017753.1017792

J. Colaço and M. Pouzet, Clocks as First Class Abstract Types, Int. Conf. On Embedded Software (EMSOFT), pp.134-155, 2003.
DOI : 10.1007/978-3-540-45212-6_10

P. Cousot, R. Cousot, and L. Mauborgne, Logical abstract domains and interpretations The Future of Software Engineering, pp.48-71, 2010.

C. Elliott and P. Hudak, Functional reactive animation, Int. Conf. Func. Prog. (ICFP). ACM, 1997.
DOI : 10.1145/258949.258973
URL : http://www.cs.yale.edu/HTML/YALE/CS/HyPlans/hudak-paul/hudak-dir/fran/icfp97.ps

C. M. Elliott, Push-pull functional reactive programming, Proceedings of the 2nd ACM SIGPLAN symposium on Haskell, Haskell '09, pp.25-36, 2009.
DOI : 10.1145/1596638.1596643

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Hughes, Programming with Arrows, Advanced Functional Programming, pp.73-129, 2005.
DOI : 10.1007/11546382_2

D. Janin, Spatio-temporal domains : an overview, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01634897

D. K. Kaynar, N. Lynch, R. Segala, and F. Vaandrager, The Theory of Timed I/O Automata, Synthesis Lectures on Computer Science, vol.21, issue.2, 2006.
DOI : 10.1109/32.345827

X. Liu and E. A. Lee, CPO semantics of timed interactive actor networks, Theoretical Computer Science, vol.409, issue.1, pp.110-125, 2008.
DOI : 10.1016/j.tcs.2008.08.044
URL : https://doi.org/10.1016/j.tcs.2008.08.044

X. Liu, E. Matsikoudis, and E. A. Lee, Modeling timed concurrent systems using generalized ultrametrics, Conf. on Conc. Theory (CONCUR), 2006.
DOI : 10.1007/11817949_1

L. Mandel and M. Pouzet, ReactiveML, a reactive extension to ML, Int. Symp. on Principles and Practice of Declarative Programming (PPDP), 2005.
URL : https://hal.archives-ouvertes.fr/hal-01489747

E. Matsikoudis and E. A. Lee, The fixed-point theory of strictly causal functions, Theoretical Computer Science, vol.574, pp.39-77, 2015.
DOI : 10.1016/j.tcs.2015.01.036

D. S. Scott, Data types as lattices, International Summer Institute and Logic Colloquium, pp.579-651, 1975.
DOI : 10.1137/0205037

P. Wadler, Propositions as sessions, Journal of Functional Programming, vol.16, issue.2-3, pp.384-418, 2014.
DOI : 10.1016/0304-3975(87)90045-4
URL : http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-sessions/propositions-as-sessions.pdf

A. Charguéraud, The Locally Nameless Representation, Journal of Automated Reasoning, vol.40, issue.12, pp.363-408, 2012.
DOI : 10.1007/s10817-008-9097-2

N. De-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indagationes Mathematicae (Proceedings), vol.75, issue.5, pp.381-392, 1972.
DOI : 10.1016/1385-7258(72)90034-0

S. Diehl, P. Hartel, and P. Sestoft, Abstract machines for programming language implementation, Future Generation Computer Systems, vol.16, issue.7, pp.739-751, 2000.
DOI : 10.1016/S0167-739X(99)00088-6
URL : http://rw4.cs.uni-sb.de/~diehl/pubs/articleDiehlHartelSestoft.pdf

C. Fournet and G. Gonthier, The reflexive CHAM and the join-calculus, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.372-385, 1996.
DOI : 10.1145/237721.237805

C. Fournet, G. Gonthier, J. Levy, L. Maranget, and D. Rémy, A calculus of mobile agents, pp.406-421, 1996.
DOI : 10.1007/3-540-61604-7_67

F. Germain, M. Lacoste, and J. Stefani, An Abstract Machine for a Higher-Order Distributed Process Calculus, Foundations of Wide Area Network Computing (ICALP 2002 Satellite Workshop), pp.145-169, 2002.
DOI : 10.1016/S1571-0661(04)80420-1

O. Kiselyov, The Design and Implementation of BER??MetaOCaml, Functional and Logic Programming -12th International Symposium, FLOPS 2014 Proceedings, pp.86-102, 2014.
DOI : 10.1007/978-3-319-07151-0_6

J. Krivine, A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, pp.199-207, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00154508

I. Lanese, J. A. Peréz, D. Sangiorgi, and A. Schmitt, On the Expressiveness and Decidability of Higher-Order Process Calculi, 23rd Annual IEEE Symposium on Logic in Computer Science Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science, pp.145-155, 2008.
URL : https://hal.archives-ouvertes.fr/hal-01112294

P. Maksimovic and A. Schmitt, HOCore in Coq, Interactive Theorem Proving -6th International Conference Proceedings, pp.278-293, 2015.
DOI : 10.1007/978-3-319-22102-1_19
URL : https://hal.archives-ouvertes.fr/hal-01099130

R. Milner, A Calculus of Communicating Systems, 1982.
DOI : 10.1007/3-540-10235-3

D. Pous, Using bisimulation proof techniques for the analysis of distributed abstract machines, Theoretical Computer Science, vol.402, issue.2-3, 2008.
DOI : 10.1016/j.tcs.2008.04.035

D. Sangiorgi, Expressing mobility in process algebras : first-order and higher-order paradigms, 1993.

D. Sangiorgi and A. Valente, A Distributed Abstract Machine for Safe Ambients, Proceedings of the 28th International Colloquium on Automata, Languages and Programming , ICALP '01, pp.408-420, 2001.
DOI : 10.1007/3-540-48224-5_34

C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, and X. Urbain, Certified Impossibility Results for Byzantine-Tolerant Mobile Robots, International Symposium on Stabilization, Safety, and Security of Distributed Systems, p.15, 2013.
DOI : 10.1007/978-3-319-03089-0_13
URL : https://hal.archives-ouvertes.fr/hal-00834633

A. Bauer, The hydra game. math.andrej.com, 2008.

P. Castéran and V. Filou, Tasks, types and tactics for local computation systems, Stud. Inform. Univ, vol.9, issue.1, pp.39-86, 2011.

P. Castéran, Utilisation en Coq de l'opérateur de description, Actes des Journées Francophones des Langages Applicatifs, 2007.

P. Castéran and É. Contéjean, On ordinal notations. User Contributions to the Coq Proof Assistant, 2006.

P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain, Impossibility of gathering, a certification, Information Processing Letters, vol.115, issue.3, pp.447-452, 2015.
DOI : 10.1016/j.ipl.2014.11.001
URL : https://hal.archives-ouvertes.fr/hal-00995126

N. Dershowitz and G. Moser, The Hydra Battle Revisited, Rewriting, Computation and Proof : Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, pp.1-27, 2007.
DOI : 10.1007/978-3-540-73147-4_1

J. Grimm, Implementation of three types of ordinals in Coq
URL : https://hal.archives-ouvertes.fr/hal-00911710

J. Ketonen and R. Solovay, Rapidly Growing Ramsey Functions, The Annals of Mathematics, vol.113, issue.2, pp.267-314, 1981.
DOI : 10.2307/2006985

L. Kirby and J. Paris, Accessible Independence Results for Peano Arithmetic, Bulletin of the London Mathematical Society, vol.14, issue.4, pp.725-731, 1982.
DOI : 10.1112/blms/14.4.285
URL : http://blms.oxfordjournals.org/cgi/reprint/14/4/285.pdf

P. Manolios and D. Vroon, Ordinal Arithmetic: Algorithms and Mechanization, Journal of Automated Reasoning, vol.9, issue.2, pp.387-423, 2005.
DOI : 10.1017/CBO9781139168717

M. Norrish and B. Huffman, Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ?? 1, International Conference on Interactive Theorem Proving, pp.133-146, 2013.
DOI : 10.1007/978-3-642-39634-2_12

M. Vinícius, M. Ramos, R. J. De-queiroz, N. Moreira, and J. Almeida, Formalization of the pumping lemma for context-free languages, 1510.

S. Schmitz, Complexity hierarchies beyond elementary. CoRR, abs/1312, 2013.
DOI : 10.1145/2858784
URL : https://hal.archives-ouvertes.fr/hal-01267354

K. Schutte, Proof theory / Translation from the German by, 1977.

W. Sladek, The Termite and the Tower : Goodstein sequences and provability in PA, 2007.

V. Buterin, A next-generation smart contract and decentralized application platform, 2014.

F. Fleutot, Lamtez : a typed lambda-calculus for tezos

L. M. Goodman, A self-amending crypto-ledger. tezos white paper, 2014.

S. Nakamoto, Bitcoin : A peer-to-peer electronic cash system, 2008.

J. Pöial, Algebraic specification of stack effects for forth programs, 1990.

J. Vouillon, V. Balat, ]. E. Anceaume, R. Ludinard, M. Potop-butucaru et al., From Bytecode to JavaScript : the Js of ocaml Compiler References Bitcoin a distributed shared register, Stabilization, Safety, and Security of Distributed Systems -19th International Symposium, SSS 2017 Proceedings, pp.456-468, 2013.

A. W. Appel and E. W. Felten, Proof-carrying authentication, Proceedings of the 6th ACM conference on Computer and communications security , CCS '99, pp.52-62, 1999.
DOI : 10.1145/319709.319718
URL : http://www.cs.princeton.edu/~appel/papers/says.ps

M. Atzei, T. Bartoletti, and . Cimoli, A Survey of Attacks on Ethereum Smart Contracts (SoK), Conference on Principles of Security and Trust, 2017.
DOI : 10.5210/fm.v2i9.548

V. Bernat, H. Ruess, and N. Shankar, First-order cyberlogic, 2005.

M. Blaze, J. Feigenbaum, and A. D. Keromytis, Keynote: Trust management for public-key infrastructures (position paper), Security Protocols, 6th International Workshop Proceedings, pp.59-63, 1998.
DOI : 10.1007/3-540-49135-x_9
URL : http://www1.cs.columbia.edu/~angelos/Papers/keynote-position.pdf

M. Blaze, J. Feigenbaum, and M. Strauss, Compliance checking in the PolicyMaker trust management system, pp.254-274, 1998.
DOI : 10.1007/BFb0055488

T. Crain, V. Gramoli, M. Larrea, and M. , (leader/randomization/signature)-free byzantine consensus for consortium blockchains Analysis of the dao exploit, 2016.

C. Dannen, Introducing Ethereum and Solidity: Foundations of Cryptocurrency and Blockchain Programming for Beginners, 2017.
DOI : 10.1007/978-1-4842-2535-6

S. Fenech, G. J. Pace, and G. Schneider, CLAN: A Tool for Contract Analysis and Conflict Discovery, pp.90-96, 2009.
DOI : 10.1007/978-3-642-04761-9_8

J. A. Garay, A. Kiayias, and N. Leonardos, The Bitcoin Backbone Protocol: Analysis and Applications, pp.281-310, 2015.
DOI : 10.1007/978-3-662-46803-6_10

L. Goodman, A self-amending crypto-ledger. tezos white paper, 2014.

N. Li, B. N. Grosof, and J. Feigenbaum, A Practically Implementable and Tractable Delegation Logic, Proceedings of the 2000 IEEE Symposium on Security and Privacy, pp.27-42, 2000.
DOI : 10.2139/ssrn.290100

P. Mcnamara, Deontic logic, 2014.
DOI : 10.1016/S1874-5857(06)80029-4

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, Conference on Automated Deduction: Automated Deduction, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217
URL : http://www.csl.sri.com/papers/c/a/cade92-pvs/cade92-pvs.ps.gz

H. Prakken and G. Sartor, The Role of Logic in Computational Models of Legal Argument: A Critical Survey, pp.342-381, 2002.
DOI : 10.1007/3-540-45632-5_14

N. Rueß, ]. J. Shankar, and . Stark, Introducing cyberlogic Making sense of blockchain smart contracts, HCSS'03?High Confidence Software and Systems Conference, 2003.

D. Tapscott and A. Tapscott, The blockchain revolution:how the technology behind bitcoin is changing Money,Business and the World Ethereum: A secure decentralised generalised transaction ledger, pp.72-2016

W. Yao, Trust management for widely distributed systems, 2004.

T. Altenkirch, N. A. Danielsson, and N. Kraus, Partiality, revisited -the partiality monad as a quotient inductive-inductive type, Foundations of Software Science and Computation Structures -20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software Proceedings, pp.534-549, 2017.

P. Audebaud and C. Paulin-mohring, Proofs of randomized algorithms in Coq, MPC, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00431771

A. Bauer, First Steps in Synthetic Computability Theory, Electronic Notes in Theoretical Computer Science, vol.155, pp.5-31, 2006.
DOI : 10.1016/j.entcs.2005.11.049

A. Bauer, J. Gross, P. Lefanu-lumsdaine, and M. Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT library, 2016.

A. Bauer and D. Lesnik, Metric spaces in synthetic topology, Annals of Pure and Applied Logic, vol.163, issue.2, pp.87-100, 2012.
DOI : 10.1016/j.apal.2011.06.017

. Santiago-zanella-béguelin, Formal certification of game-based cryptographic proofs, 2010.

T. Coquand and B. Spitters, Integrals and valuations, Journal of Logic and Analysis, vol.1, issue.3, pp.1-22, 2009.

M. Escardó, Synthetic Topology, Electronic Notes in Theoretical Computer Science, vol.87, pp.21-156, 2004.
DOI : 10.1016/j.entcs.2004.09.017

M. Escardó and C. Knapp, Partial elements and recursion via dominances in univalent type theory, 2017.

G. Gilbert, Formalising real numbers in homotopy type theory. CPP'17, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01449326

M. Giry, A categorical approach to probability theory In Categorical aspects of topology and analysis, pp.68-85, 1982.

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

O. Hasan-andsofì-ene-tahar, Formalization of Continuous Probability Distributions, pp.3-18, 2007.

J. Hölzl, Markov processes in isabelle/hol, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp.100-111, 2017.

D. Huang and G. Morrisett, An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages, European Symposium on Programming Languages and Systems, pp.337-363, 2016.
DOI : 10.1007/978-3-642-56999-9

M. Hyland, First steps in synthetic domain theory, Category Theory, pp.131-156, 1991.
DOI : 10.1007/BFb0018350

C. Jones and G. Plotkin, A probabilistic powerdomain of evaluations, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1989.
DOI : 10.1109/LICS.1989.39173

D. Kozen, Semantics of probabilistic programs, Journal of Computer and System Sciences, vol.22, issue.3, pp.328-350, 1981.
DOI : 10.1016/0022-0000(81)90036-2

R. Krebbers and B. Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, vol.9, issue.1, pp.1-27, 2013.
DOI : 10.2168/LMCS-9(1:1)2013

D. Le?nik, Synthetic topology and constructive metric spaces. Diss, 2010.

P. Lietz, From constructive mathematics to computable analysis via the realizability interpretation, 2005.

M. Mayero, Formalisation et automatisation de preuves en analyses réelle et numérique, 2001.

E. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.14-23, 1989.
DOI : 10.1109/LICS.1989.39155
URL : http://pfp7.is.ocha.ac.jp/~ichikawa/ppe/ftp/moggi/lc88.ps

O. Russell and . Connor, Certified Exact Transcendental Real Number Computation in Coq, pp.246-261, 2008.

N. Ramsey and A. Pfeffer, Stochastic lambda calculus and monads of probability distributions, ACM SIGPLAN Notices, pp.154-165, 2002.

E. Rijke and B. Spitters, Sets in homotopy type theory, MSCS, special issue : From type theory and homotopy theory to univalent foundations, 2014.
DOI : 10.1093/logcom/14.4.447

T. Sato, Approximate Relational Hoare Logic for Continuous Random Samplings, Electronic Notes in Theoretical Computer Science, vol.325, pp.277-298, 2016.
DOI : 10.1016/j.entcs.2016.09.043
URL : https://doi.org/10.1016/j.entcs.2016.09.043

M. Shulman, Brouwer's fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science, vol.38, 2015.
DOI : 10.1016/j.apal.2016.04.010

B. Spitters and E. Van-der-weegen, Type classes for mathematics in type theory. MSCS, special issue on 'Interactive theorem proving and the formalization of mathematics, pp.1-31, 2011.

S. Vickers-]-patrick-baudin, J. Filliâtre, C. Marché, B. Monate, Y. Moy et al., A monad of valuation locales ACSL : ANSI/ISO C Specification Language, version 1, 2009.

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Let???s verify this with Why3, International Journal on Software Tools for Technology Transfer, vol.7, issue.5, pp.709-727, 2015.
DOI : 10.1007/978-3-642-02959-2_10

R. Burstall, Some techniques for proving correctness of programs which alter data structures, Machine Intelligence, vol.7, pp.23-50, 1972.

A. Charguéraud and F. Pottier, Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits, Journal of Automated Reasoning, vol.18, issue.9, 2017.
DOI : 10.1145/361002.361016

M. Clochard, J. Filliâtre, and A. Paskevich, How to Avoid Proving the Absence of Integer Overflows, 7th Working Conference on Verified Software : Theories, Tools and Experiments (VSTTE), pp.94-109, 2015.
DOI : 10.1007/978-3-319-08867-9_1
URL : https://hal.archives-ouvertes.fr/hal-01162661

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, Theorem Proving in Higher Order Logics (TPHOLs), 2009.
DOI : 10.1007/978-3-540-74591-4_15

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, Proceedings of the 10th International Conference on Software Engineering and Formal Methods, number 7504 in Lecture Notes in Computer Science, pp.233-247, 2012.
DOI : 10.1007/978-3-642-33826-7_16

J. Filliâtre, One Logic to Use Them All, 24th International Conference on Automated Deduction, pp.1-20, 2013.
DOI : 10.1007/978-3-642-38574-2_1

J. Filliâtre, Le petit guide du bouturage, ou comment réaliser des arbres mutables en OCaml, Vingt-cinquièmes Journées Francophones des Langages Applicatifs, 2014.

J. Filliâtre, L. Gondelman, and A. Paskevich, A pragmatic type system for deductive verification, Research report, 2016.

J. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code. Formal Methods in System Design, pp.152-174, 2016.

J. Filliâtre and C. Marché, Multi-prover Verification of C Programs, Sixth International Conference on Formal Engineering Methods, pp.15-29, 2004.
DOI : 10.1007/978-3-540-30482-1_10

T. Hubert and C. Marché, A case study of C source code verification: the Schorr-Waite algorithm, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005.
DOI : 10.1109/SEFM.2005.1

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx et al., VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, NASA Formal Methods, pp.41-55, 2011.
DOI : 10.1007/11691372_19

K. Rustan and M. Leino, Dafny : An automatic program verifier for functional correctness, LPAR- 16, pp.348-370, 2010.

W. Reif, G. Schnellhorn, and K. Stenzel, Proving System Correctness with KIV 3.0, 14th International Conference on Automated Deduction, pp.69-72, 1997.
DOI : 10.1007/3-540-63104-6_10

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002.
DOI : 10.1109/LICS.2002.1029817

H. Schorr and W. M. Waite, An efficient machine-independent procedure for garbage collection in various list structures, Communications of the ACM, vol.10, issue.8, pp.501-506, 1967.
DOI : 10.1145/363534.363554

S. Boldo, F. Clément, F. Faissole, V. Martin, and M. Mayero, A Coq Formal Proof of the Lax?Milgram theorem, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.79-89, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01391578

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.24, issue.9, pp.41-62, 2015.
DOI : 10.1109/32.713327
URL : https://hal.archives-ouvertes.fr/hal-00860648

F. Clément and V. Martin, The Lax-Milgram Theorem. A detailed proof to be formalized in Coq, 2016.

C. Cohen and D. Rouhling, A Formal Proof in Coq of LaSalle???s Invariance Principle, Interactive Theorem Proving, 2017.
DOI : 10.1007/978-3-540-71067-7_20

J. and D. Mallagaray, Formalisation and execution of Linear Algebra : theorems and algorithms, 2016.

F. Faissole, Formalization and closedness of finite dimensional subspaces, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01630411

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, Interactive Theorem Proving -4th International Conference Proceedings, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

J. Harrison, A HOL Theory of Euclidean Space, Theorem Proving in Higher Order Logics, 18th International Conference, 2005.
DOI : 10.1007/11541868_8

A. Mahboubi, The Rooster and the Butterflies, CICM 2013 -Conference on Intelligent Computer Mathematics - 2013, pp.1-18, 2013.
DOI : 10.1007/978-3-642-39320-4_1
URL : https://hal.archives-ouvertes.fr/hal-00825074

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, Interactive Theorem Proving - 4th International Conference, ITP 2013 Proceedings, pp.19-34, 2013.
DOI : 10.1007/978-3-642-39634-2_5
URL : https://hal.archives-ouvertes.fr/hal-00816703

M. Y. Mahmoud, V. Aravantinos, and S. Tahar, Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory, NASA Formal Methods, 5th International Symposium, NFM 2013. Proceedings, pp.413-427, 2013.
DOI : 10.1007/978-3-642-38088-4_28

G. Barany, Liveness-driven random program generation Frama-C : A software analysis perspective, 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), pp.573-609, 2015.

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

F. Nielson, H. R. Nielson, and C. Hankin, Principles of Program Analysis, 1999.
DOI : 10.1007/978-3-662-03811-6

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, PLDI '11, pp.283-294, 2011.

A. Abel, B. Pientka, D. Thibodeau, and A. Setzer, Copatterns, ACM SIGPLAN Notices, vol.48, issue.1, pp.27-38, 2013.
DOI : 10.1145/1328438.1328482

P. Laforgue and Y. Régis-gianas, Copattern matching and first-class observations in OCaml, with a macro, Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming , PPDP '17, pp.97-108, 2017.
DOI : 10.1145/1328438.1328482
URL : https://hal.archives-ouvertes.fr/hal-01653261

]. I. Androutsopoulos, G. D. Ritchie, and P. Thanisch, Natural language interfaces to databases ??? an introduction, Natural Language Engineering, vol.14, issue.01, pp.29-81, 1995.
DOI : 10.1145/319983.319986

D. G. Bobrow, R. M. Kaplan, M. Kay, D. A. Norman, H. Thompson et al., GUS, a frame-driven dialog system, Artificial Intelligence, vol.8, issue.2, pp.155-173, 1977.
DOI : 10.1016/0004-3702(77)90018-2

T. Bourke and M. Pouzet, The checklistings package, 2015.

M. J. Boyer and H. Mili, Agile business rule development, Agile Business Rule Development, pp.49-71, 2011.
DOI : 10.1007/978-3-642-19041-4
URL : https://link.springer.com/content/pdf/bfm%3A978-3-642-19041-4%2F1.pdf

. Facebook, Messenger platform, 2017. https://developers.facebook.com/docs/ messenger-platform, 2017.

. Facebook, Messenger platform, 2017. https://developers.facebook.com/docs/ messenger-platform, 2017.

. Google, Google translate service, 2017.

M. Jambon, atdgen documentation, 2017.

D. Jurafsky and J. H. Martin, Speech and Language Processing, 2009.

R. Kaplan, Beyond the GUI: It's time for a conversational user interface, 2013.

B. Lucas, VoiceXML for Web-based distributed conversational applications, Communications of the ACM, vol.43, issue.9, pp.53-57, 2000.
DOI : 10.1145/348941.348985

L. Mandel, C. Pasteur, and M. Pouzet, ReactiveML, ten years later, Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP '15, 2015.
DOI : 10.1145/800087.802786
URL : https://hal.archives-ouvertes.fr/hal-01508179

M. F. Mctear, Spoken dialogue technology: enabling the conversational user interface, ACM Computing Surveys, vol.34, issue.1, pp.90-169, 2002.
DOI : 10.1145/505282.505285

. Microsoft, Bot framework documentation, 2017.

A. Patil, K. Marimuthu, and R. Niranchana, Comparative study of cloud platforms to develop a Chatbot, International Journal of Engineering & Technology, vol.6, issue.3, pp.57-61, 2017.
DOI : 10.14419/ijet.v6i3.7628

. Spring, Spring expression language (SpEL), 2017. https://docs.spring.io/spring-framework/ docs/current/spring-framework-reference/core.html#expressions, 2017.

J. D. Williams, N. B. Niraula, P. Dasigi, A. Lakshmiratan, C. G. Suarez et al., Rapidly Scaling Dialog Systems with Interactive Learning, International Workshop on Spoken Dialog Systems, 2015.
DOI : 10.1109/MSP.2005.1511821

A. R. Bradley and Z. Manna, The Calculus of Computation : Decision Procedures with Applications to Verification (Chapters 5, 2007.

R. Brummayer and A. Biere, Lemmas on demand for the extensional theory of arrays, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, SMT '08/BPR '08, pp.165-201, 2009.
DOI : 10.1145/1512464.1512467

C. Cadar and K. Sen, Symbolic execution for software testing, Communications of the ACM, vol.56, issue.2, pp.82-90, 2013.
DOI : 10.1145/2408776.2408795

E. M. Clarke, D. Kroening, and F. Lerda, A Tool for Checking ANSI-C Programs, TACAS, pp.168-176, 2004.
DOI : 10.1007/978-3-540-24730-2_15

R. David, S. Bardin, J. Feist, L. Mounier, M. Potet et al., Specification of concretization and symbolization policies in symbolic execution, Proceedings of the 25th International Symposium on Software Testing and Analysis, ISSTA 2016, pp.36-46, 2016.
DOI : 10.1109/ASE.2004.1342749

R. David, S. Bardin, T. D. Ta, L. Mounier, J. Feist et al., BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis, 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER), pp.653-656, 2016.
DOI : 10.1109/SANER.2016.43

P. J. Downey and R. Sethi, Assignment Commands with Array References, Journal of the ACM, vol.25, issue.4, pp.652-666, 1978.
DOI : 10.1145/322092.322104

V. Ganesh and D. L. Dill, A Decision Procedure for Bit-Vectors and Arrays, CAV, pp.519-531, 2007.
DOI : 10.1007/978-3-540-73368-3_52

P. Godefroid, N. Klarlund, and K. Sen, DART : directed automated random testing, PLDI, pp.213-223, 2005.

D. Kroening and O. Strichman, Decision Procedures -An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, 2008.

P. Baudin, J. Filliâtre, C. Marché, B. Monate, Y. Moy et al., ACSL : ANSI/ISO C specification language, 2008.

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3 : Shepherd your herd of provers, Boogie 2011 : First International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

J. Filliâtre, One Logic to Use Them All, 24th International Conference on Automated Deduction, pp.1-20, 2013.
DOI : 10.1007/978-3-642-38574-2_1

J. Filliâtre, L. Gondelman, and A. Paskevich, A pragmatic type system for deductive verification, Research report, 2016.

J. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code. Formal Methods in System Design, pp.152-174, 2016.

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

K. Rustan, M. Leino, and M. Moskal, Usable auto-active verification, Usable Verification Workshop, 2010.

R. Rieu-helft, C. Marché, and G. Melquiond, How to Get an Efficient yet Verified Arbitrary-Precision Integer Library, 9th Working Conference on Verified Software : Theories, Tools, and Experiments, 2017.
DOI : 10.1109/CSF.2016.28
URL : https://hal.archives-ouvertes.fr/hal-01519732

E. Al-shaer, S. Al-haj, and . Flowchecker, Configuration Analysis and Verification of Federated OpenFlow Infrastructures, Proceedings of the 3rd ACM Workshop on Assurable and Usable Security Configuration (CCS'10), 2010.

T. Ball, N. Bjørner, A. Gember, S. Itzhaky, A. Karbyshev et al., Vericon : Towards Verifying Controller Programs in Software-Defined Networks, Proc. 35th ACM SIGPLAN Intl. Conf. Programming Language Design (PLDI'14), pp.282-293, 2014.

T. Bouton, D. Caminha-barbosa-de-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, Proc. 22nd International Conference on Automated Deduction (CADE-22), pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti et al., The nuXmv Symbolic Model Checker, Proc. 26th Intl. Conf. Computer Aided Verification, pp.334-342, 2014.
DOI : 10.1007/978-3-319-08867-9_22

N. Feamster, J. Rexford, and E. Zegura, The road to SDN, ACM SIGCOMM Computer Communication Review, vol.44, issue.2, pp.87-98, 2014.
DOI : 10.1145/2602204.2602219

N. Foster, M. J. Freedman, A. Guha, and R. Harrison, Languages for software-defined networks, Software Technology Group, 2016.
DOI : 10.1109/MCOM.2013.6461197
URL : http://www.cs.princeton.edu/~mfreed/docs/frenetic-ieeecomm13.pdf

G. Hurel, R. Badonnel, A. Lahmadi, and O. Festor, Behavioral and dynamic security functions chaining for Android devices, 2015 11th International Conference on Network and Service Management (CNSM), 2015.
DOI : 10.1109/CNSM.2015.7367339
URL : https://hal.archives-ouvertes.fr/hal-01231173

A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P. Brighten, VeriFlow : Verifying Network-wide Invariants in Real Time, Proceedings of the first Workshop on Hot Topics in Software-Defined Networks (HotSDN'12), 2012.

H. Kim, J. Reich, A. Gupta, M. Shahbaz, N. Feamster et al., Kinetic : Verifiable Dynamic Network Control, Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation (NSDI'15), 2015.
DOI : 10.1002/sec.1317

N. Mckeown and G. Parulkar, openflow, enabling innovation in campus networks, In ACM SIGCOMM Computer Communication Review, 2008.

N. Schnepf, S. Merz, R. Badonnel, and A. Lahmadi, Automated verification of security chains in software-defined networks with synaptic, 2017 IEEE Conference on Network Softwarization (NetSoft), 2017.
DOI : 10.1109/NETSOFT.2017.8004195
URL : https://hal.archives-ouvertes.fr/hal-01630806

. Why3-a-dit, Références [1] Why3, a tool for deductive program verification, GNU LGPL 2.1. http://why3.lri.fr. [2] Formalization of relaxed slicing, 2016.

R. W. Barraclough, D. Binkley, S. Danicic, M. Harman, R. M. Hierons et al., A trajectory-based strict semantics for program slicing, Theoretical Computer Science, vol.411, issue.11-13, pp.11-131372, 2010.
DOI : 10.1016/j.tcs.2009.10.025

J. Bernardo-barros, D. Carneiro-da-cruz, P. R. Henriques, and J. S. Pinto, Assertion-based slicing and slice graphs, 2010.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Danicic, R. W. Barraclough, M. Harman, J. Howroyd, Á. Kiss et al., A unifying theory of control dependence and its application to arbitrary program structures, Theoretical Computer Science, vol.412, issue.49, pp.6809-6842, 2011.
DOI : 10.1016/j.tcs.2011.08.033

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, ESOP, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

M. Harman, D. Binkley, and S. Danicic, Amorphous program slicing, Journal of Systems and Software, vol.68, issue.1, pp.45-64, 2003.
DOI : 10.1016/S0164-1212(02)00135-8
URL : http://www.brunel.ac.uk/~csstmmh2/jss1.ps

J. Léchenet, N. Kosmatov, and P. L. Gall, Cut branches before looking for bugs : Sound verification on relaxed slices, FASE'16 (Part of ETAPS'16), pp.179-196, 2016.

J. Léchenet, N. Kosmatov, and P. L. Gall, Fast computation of arbitrary control dependencies, 2018.

J. Léchenet, N. Kosmatov, and P. L. Gall, Coq a dit : fromage tranché ne peut cacher ses trous, Vingt-septièmes Journées Francophones des Langages Applicatifs, p.2016, 2016.

F. Tip, A survey of program slicing techniques, J. Prog. Lang, vol.3, issue.3, 1995.

M. Weiser, Program Slicing, IEEE Transactions on Software Engineering, vol.10, issue.4, 1979.
DOI : 10.1109/TSE.1984.5010248

M. Weiser, Program Slicing, ICSE 1981, 1981.
DOI : 10.1109/TSE.1984.5010248