S. Boutin, Using reflection to build efficient and certified decision procedures, 3rd International Symposium on Theoretical Aspects of Computer Software (TACS), vol.1281, pp.515-529, 1997.

W. J. Cody, J. , and W. Waite, Software Manual for the Elementary Functions, 1980.

M. Daumas and G. Melquiond, Certification of bounds on expressions involving rounded operators, ACM Transactions on Mathematical Software, vol.37, issue.1, pp.1-20, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00127769

, IEEE standard for floating-point arithmetic, IEEE Computer Society, 2008.

A. Mahboubi, G. Melquiond, and T. Sibut-pinote, Formally verified approximations of definite integrals, Journal of Automated Reasoning, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01289616

É. Martin, -. , and G. Melquiond, Proving tight bounds on univariate expressions with elementary functions in Coq, Journal of Automated Reasoning, vol.57, issue.3, pp.187-217, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01086460

J. Muller, N. Brunie, C. Florent-de-dinechin, M. Jeannerod, V. Joldes et al., Nathalie Revol, and Serge Torres. Handbook of FloatingPoint Arithmetic. Birkhäuser Basel, 2018.

R. Skeel, Roundoff error cripples Patriot missile, SIAM News, vol.25, issue.4, p.11, 1992.

A. Solovyev, C. Jacobsen, Z. Rakamari?, and G. Gopalakrishnan, Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions, 20th International Symposium on Formal Methods (FM), vol.9109, pp.532-555, 2015.

, COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (BETTY), 2012.

D. Ancona, V. Bono, M. Bravetti, G. Castagna, J. Campos et al., Behavioral Types in Programming Languages, Foundations and Trends in Programming Languages, vol.3, issue.2-3, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01348054

M. Bartoletti, I. Castellani, P. Deniélou, M. Dezani-ciancaglini, S. Ghilezan et al., Combining behavioural types with security analysis, Journal of Logical and Algebraic Methods in Programming, vol.84, issue.6, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01213201

K. Honda, V. Vasconcelos, and M. Kubo, Language primitives and type discipline for structured communication-based programming, Proc. ESOP'98, vol.1381, 1998.

K. Honda, N. Yoshida, and M. Carbone, Multiparty asynchronous session types, Proc. POPL'08, pp.273-284, 2008.

H. Hüttel, I. Lanese, V. T. Vasconcelos, L. Caires, M. Carbone et al., Foundations of Session Types and Behavioural Contracts, ACM Computing Surveys, vol.49, issue.1, 2016.

, Behavioural Types: from Theory to Tools, 2017.

G. Berry, Real time programming : Special purpose or general purpose languages. Information Processing, vol.89, pp.11-17, 1989.
URL : https://hal.archives-ouvertes.fr/inria-00075494

P. Caspi, Lucid synchrone
URL : https://hal.archives-ouvertes.fr/hal-01574464

C. Invitée,

G. Hamon and M. Pouzet, Un simulateur synchrone pour Lucid Synchrone
URL : https://hal.archives-ouvertes.fr/hal-01574461

F. Loulergue, Extension du BSlambda-calcul

B. Marre and A. Arnould, Génération automatique de séquences de testsàtests`testsà partir de descriptions Lustre : GATeL

F. Boniol, G. Bel, and J. Foiseau, Modélisation et vérification de systèmes intégrés asynchrones dans le langage synchrone Lustre : application aux systèmes avioniques

J. Serot, Un compilateur CAML ? SYNDEX pour les applications de traitement de signal temps-réel distribués

R. Kieburtz, Coalgebraic techniques for reactive functional programming

C. Invitée,

P. Cuoq and M. Pouzet, Causalité modulaire dans un langage de flots synchrone, Douzì emes Journées Francophones des Langages Applicatifs, 2001.

O. Michel, J. Giavitto, and J. Cohen, MGS : transformer des collections complexes pour la simulation en biologie, Rideau-Gallot, vol.70

A. Merlin and G. Hains, La machine abstraite catégorique BSP, Rideau-Gallot, vol.70

J. Cohen, O. Michel, and J. Giavitto, Filtrage et r` egles de réécriture sur des structures indexées par des groupes

Y. Ait-ameur, F. Boniol, S. Pairault, and V. Wiels, Analyse de robustesse de systèmes avioniques

F. Gava and F. Loulergue, Synthèse de types pour Bulk Synchronous Parallel ML

F. Gava, Une bibliothèque certifiée de programmes fonctionnels BSP, Quinzì emes Journées Francophones des Langages Applicatifs, 2004.
DOI : 10.3166/tsi.25.1261-1280

L. Mandel and M. Pouzet, ReactiveML, un langage pour la programmation réactive en ML, Seizì emes Journées Francophones des Langages Applicatifs (JFLA 2005), 2005.
DOI : 10.3166/tsi.27.1097-1128

R. Benheddi and F. Loulergue, Sémantiques de MSPML avec compositionparalì ele, Dixseptì emes Journées Francophones des Langages Applicatifs (JFLA 2006), 2006.

M. Pouzet, Programmation synchrone fonctionnelle, Dix-huitì emes Journées Francophones des Langages Applicatifs, 2007.

P. Synchrone-aux, J. G. Baudart, L. Mandel, and E. M. Pouzet,

L. Mandel and F. Plateau, Abstraction d'horloges dans les systèmes synchrones flot de données, Vingtì emes Journées Francophones des Langages Applicatifs, 2009.

L. Mandel, F. Plateau, and M. Pouzet, Lucy-n : une extension n-synchrone de Lustre
URL : https://hal.archives-ouvertes.fr/hal-00545802

L. Mandel, Cours de ReactiveML

L. Mandel and F. Plateau, Typage des horloges périodiques en Lucy-n, Conchon, vol.67

F. Gava and S. Tan, Implémentation et prédiction des performances de squelettes dataparalì eles en utilisant un langage BSP de haut niveau

W. Bousdira, F. Loulergue, and L. Gesbert, Syntaxe et sémantique de revised Bulk Synchronous Parallel ML, Conchon, vol.67

T. Braibant, De coquets circuits, Conchon, vol.67

C. Deleuze, Concurrence et continuations en OCaml, Vingt troisì emes Journées Francophones des Langages Applicatifs (JFLA 2012), 2012.
URL : https://hal.archives-ouvertes.fr/hal-00665918

L. Mandel and C. Pasteur, Réactivité des systèmes coopératifs : le cas de ReactiveML

C. Deleuze, Concurrence légère en OCaml : muthreads

A. Guatto and L. Mandel, Réseaux de KahnàKahn`Kahnà rafales et horlogesentì eres

L. Mandel and C. Pasteur, Exécution efficace de programmes ReactiveML

L. Mandel and M. Pouzet, ReactiveML, un langage de programmation réactif

, Exposé invité parmi les contributions marquantes des dixdernì eres années)

R. E. Siba¨?esiba¨?e and E. Chailloux, Pendulum : une extension réactive pour la programmation Web en OCaml, Vingtsixì emes Journées Francophones des Langages Applicatifs, 2015.

S. Varoumas, B. Vaugon, and E. Chailloux, OCaLustre : une extension synchrone d'OCaml pour la programmation de microcontrôleurs

T. Bourke, P. Dagand, M. Pouzet, and L. Rieg, Vérification de la génération modulaire du code impératif pour Lustre

B. P. Serpette and D. Janin, Causalité dans les calculs d'´ evénements

G. Baudart, L. Mandel, O. Tardieu, and M. Vaziri, Cloudlens, un langage de script pour l'analyse de données semi-structurées

D. Janin, Domaines spatio-temporels : un tour d'horizon. In Boldo, vol.63

S. Varoumas, B. Vaugon, and E. Chailloux, La programmation de microcontrôleurs dans des langages de haut niveau

G. Baudart, L. Mandel, and J. Siméon, Programmer des chatbots en OCaml avec Watson Conversation Service

T. Bourke and M. Pouzet, Arguments cadencés dans un compilateur Lustre vérifié, Trentì emes Journées Francophones des Langages Applicatifs (JFLA 2019), 2019.

M. Pouzet, Lucid Synchrone, version 3. Tutorial and reference manual, 2006.

A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. L. Guernic et al., The synchronous languages 12 years later, Proceedings of the IEEE, vol.91, issue.1, 2003.

J. Colaco, B. Pagano, and M. Pouzet, Scade 6 : A Formal Language for Embedded Critical Software Development, Eleventh International Symposium on Theoretical Aspect of Software Engineering (TASE), 2017.
URL : https://hal.archives-ouvertes.fr/hal-01666470

P. Caspi, M. Pouzet, ;. Baudart, L. Mandel, and E. M. Pouzet, Réseaux de Kahn Synchrones, Journées Francophones des Langages Programmation Synchrone aux

(. Applicatifs and V. Morin, , 1996.

P. Caspi, Lucid synchrone, Actes du colloque INRIA OPOPAC, Lacanau, 1993.
URL : https://hal.archives-ouvertes.fr/hal-01574464

G. Hamon and M. Pouzet, Modular Resetting of Synchronous Data-flow Programs, ACM International conference on Principles of Declarative Programming (PPDP'00), 2000.
URL : https://hal.archives-ouvertes.fr/hal-01573195

G. Hamon, Calcul d'horloge et Structures de Contrôle dans Lucid Synchrone, un langage de flots synchronesàsynchrones`synchronesà la ML, 2002.

J. Colaço, B. Pagano, and M. Pouzet, A Conservative Extension of Synchronous Data-flow with State Machines, ACM International Conference on Embedded Software (EMSOFT'05), 2005.

P. Cuoq, Ajout de synchronisme dans les langages fonctionnels typés, 2002.

J. , L. Colaço, and M. Pouzet, Type-based Initialization Analysis of a Synchronous Data-flow Language, International Journal on Software Tools for Technology Transfer (STTT), vol.6, issue.3, pp.245-255, 2004.

D. Biernacki, J. Colaco, G. Hamon, and M. Pouzet, Clock-directed Modular Code Generation of Synchronous Data-flow Languages, ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), 2008.

T. Bourke and M. Pouzet, Zélus, a Synchronous Language with ODEs, International Conference on Hybrid Systems : Computation and Control (HSCC 2013), 2013.

F. Boussinot, Reactive C : An extension of C to program reactive systems, Software Practice and Experience, vol.21, issue.4, pp.401-428, 1991.

F. Boussinot and J. Susini, The SugarCubes tool box : A reactive java framework. Software Practice and Experience, vol.28, pp.1531-1550, 1998.

C. Reynolds, Flocks, herds and schools : A distributed behavioral model, Proceedings of the 14th Annual Conference on Computer Graphics and Interactive Techniques, SIGGRAPH '87, 1987.

G. Kahn and D. Macqueen, Coroutines and Networks of Parallel Processes, 1976.
URL : https://hal.archives-ouvertes.fr/inria-00306565

R. Milner, Communicating and Mobile Systems : The ?-Calculus, 1999.

P. Bjesse, K. Claessen, M. Sheeran, and S. Singh, Lava : Hardware Design in Haskell, International Conference on Functional Programming (ICFP), 1998.

C. Elliot and P. Hudak, Functional reactive animation, International Conference on Functional Programming (ICFP), 1997.

Z. Wan and P. Hudak, Functional reactive programming from first principles, International Conference on Programming Language, Design and Implementation (PLDI), 2000.

W. Taha, Multi-stage programming : Its theory and applications, 1999.

L. Mandel, C. Pasteur, M. Pouzet, and . Reactiveml, Ten Years Later, ACM International Conference on Principles and Practice of Declarative Programming (PPDP), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01508179

, INRIA, Vingtneuvì emes Journées Francophones des Langages Applicatifs (JFLA 2018), 2018.

, INRIA, Vingthuitì emes Journées Francophones des Langages Applicatifs (JFLA 2017), 2017.

, Vingtcinquì emes Journées Francophones des Langages Applicatifs (JFLA 2014), 2014.

P. Synchrone-aux, J. G. Baudart, L. Mandel, and E. M. Pouzet,

, Vingtquatrì emes Journées Francophones des Langages Applicatifs (JFLA 2013), 2013.

, Vingtdeuxì emes Journées Francophones des Langages Applicatifs, 2011.

, Vingt etunì emes Journées Francophones des Langages Applicatifs (JFLA 2010), 2010.

, INRIA, Quatorzì emes Journées Francophones des Langages Applicatifs (JFLA 2003), 2003.

, INRIA, Treizì emes Journées Francophones des Langages Applicatifs, 2002.

, INRIA, Onzì emes Journées Francophones des Langages Applicatifs, 2000.

, INRIA, Dixì emes Journées Francophones des Langages Applicatifs (JFLA 1999), 1999.

T. Arvin, Comparison of different SQL's implementations, 2017.

J. S. Auerbach, M. Hirzel, L. Mandel, A. Shinnar, and J. Siméon, Handling environments in a nested relational algebra with combinators and an implementation in a verified query compiler, SIGMOD Conference, 2017.

V. Benzaken, E. Contejean, and S. Dumbrava, A Coq Formalization of the Relational Data Model, 23rd European Symposium on Programming (ESOP), 2014.
URL : https://hal.archives-ouvertes.fr/hal-00924156

V. Benzaken, É. Contejean, C. Keller, and E. Martins, A Coq formalisation of SQL's execution engines, Int. Conf. on Interactive Theorem Proving (ITP 2018), 2018.

S. Ceri and G. Gotlob, Translating SQL into relational algebra : Optimisation, semantics, and equivalence of SQL queries, IEEE Trans., on Software Engineering, SE, vol.11, pp.324-345, 1985.

S. Chu, K. Weitz, A. Cheung, and D. Suciu, HoTTSQL : Proving query rewrites with univalent SQL semantics, PLDI. ACM, 2017.

S. Cluet and G. Moerkotte, Nested queries in object bases, Database Programming Languages, 1993.

H. Garcia-molina, J. D. Ullman, and J. Widom, Database systems-the complete book, 2009.

C. Gonzalia, Towards a formalisation of relational database theory in constructive type theory, RelMiCS, 2003.

C. Gonzalia, Relations in Dependent Type Theory, 2006.

T. J. Green, G. Karvounarakis, and V. Tannen, Provenance semirings, Proc., of the 26th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 2007.

P. Guagliardo and L. Libkin, A formal semantics of SQL queries, its validation, and applications, vol.11, pp.27-39, 2017.

R. Harper, Practical Foundations for Programming Languages, 2016.

. Iso/iec, Information technology-database languages-SQL-part 2 : Foundation (SQL/foundation), 2006.

X. Leroy, A formally verified compiler back-end, J. Autom. Reasoning, vol.43, issue.4, pp.363-446, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00360768

G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky, Toward a verified relational database management system, ACM Int. Conf. POPL, 2010.

M. Negri, G. Pelagatti, and L. Sbattella, Formal semantics of SQL queries, ACM Trans. Database Syst, vol.16, issue.3, pp.513-534, 1991.

, The Agda Development Team. The Agda Proof Assistant Reference Manual, 2010.

, The Coq Development Team. The Coq Proof Assistant Reference Manual, 2010.

, The Isabelle Development Team. The Isabelle Interactive Theorem Prover, 2010.

M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Certified Programs and Proofs, pp.135-150, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00639130

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic et al., Computer Aided Verification-23rd International Conference, vol.6806, pp.171-177, 2011.

F. Besson, ppsimpl : a reflexive Coq tactic for canonising goals, CoqPL, 2017.

D. Jasmin-christian-blanchette, C. Greenaway, D. Kaliszyk, J. Kühlwein, and . Urban, A Learning-Based Fact Selector for Isabelle/HOL, J. Autom. Reasoning, vol.57, issue.3, pp.219-244, 2016.

S. Böhme and T. Weber, Fast LCF-Style Proof Reconstruction for Z3, ITP, vol.6172, pp.179-194, 2010.

M. P. Bonacina, S. Graham-lengrand, and N. Shankar, Proofs in conflictdriven theory combination, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, vol.2018, pp.186-200, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01935595

S. Boulmé, Defensive Certification in Coq with ML Type-Safe Oracles, 2016.

S. Boulmé and A. Maréchal, Toward Certification for Free ! working paper or preprint, 2017.

L. Czajka and C. Kaliszyk, Hammer for Coq : Automation for Dependent Type Theory, J. Autom. Reasoning, vol.61, issue.1-4, pp.423-453, 2018.

B. Ekici, G. Katz, C. Keller, A. Mebsout, A. J. Reynolds et al., Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), Proceedings First International Workshop on Hammers for Type Theories, pp.21-29, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01388984

B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz et al., SMTCoq : A plug-in for integrating SMT solvers into Coq, Computer Aided Verification-29th International Conference, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01669345

J. Hurd, System Description : The Metis Proof Tactic. Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), pp.103-104, 2005.

C. Keller, Proof Technology in Mathematics Research and Teaching, chapter SMTCoq : Mixing automatic and interactive proof technologies, 2018.

S. Lescuyer, Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. (Formalisation et developpement d'une tactique reflexive pour la demonstration automatique en coq), 2011.
URL : https://hal.archives-ouvertes.fr/tel-00713668

P. Letouzey, The zify tactic

C. Paulin-mohring, Introduction to the Calculus of Inductive Constructions, All about Proofs, Proofs for All, vol.55, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01094195

C. Lawrence, J. C. Paulson, and . Blanchette, Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers, The 8th International Workshop on the Implementation of Logics, IWIL 2010, vol.2, pp.1-11, 2010.

T. Zimmermann and H. Herbelin, Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01152588

D. Biernacki, J. Colaço, G. Hamon, and M. Pouzet, Clock-directed modular code generation for synchronous data-flow languages, Proc. 9th ACM SIGPLAN Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES 2008), pp.121-130, 2008.

S. Blazy and X. Leroy, Mechanized semantics for the Clight subset of the C language, J. Automated Reasoning, vol.43, issue.3, pp.263-288, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00352524

S. Boulmé and G. Hamon, Certifying synchrony for free, R. Nieuwenhuis et A. Voronkov, éds : Proc. 8th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), vol.2250, pp.495-506, 2001.

S. Boulmé and G. Hamon, A clocked denotational semantics for Lucid-Synchrone in Coq, Rap. tech, vol.6, 2001.

T. Bourke, L. Brun, P. Dagand, X. Leroy, M. Pouzet et al., A formally verified compiler for Lustre, Proc. 2017 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp.586-601, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01512286

T. Bourke, P. Dagand, M. Pouzet, and L. Rieg, Vérification de la génération modulaire du code impératif pour Lustre, J. Signoles et S. Boldo, éds : 28 ièmes Journées Francophones des Langages Applicatifs, pp.165-179, 2017.

P. Caspi, Clocks in dataflow languages, Theor. Comp. Sci, vol.94, issue.1, pp.125-140, 1992.

J. Colaço, Private communication, 2017.

J. Colaço, B. Pagano, and M. Pouzet, Scade 6 : A formal language for embedded critical software development, Proc. 11th Int. Symp. Theoretical Aspects of Software Engineering (TASE 2017), 2017.

J. Colaço and M. Pouzet, Clocks as first class abstract types, R. Alur et I. Lee, éds : Proc. 3rd Int. Conf. on Embedded Software (EMSOFT 2003), pp.134-155, 2003.

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language LUSTRE. Proc. IEEE, vol.79, pp.1305-1320, 1991.

-. C. Programming-languages, . Standard, . Iec, . Geneva, and . Switzerland, , 1999.

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML : A verified implementation of ML, Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp.179-191, 2014.

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

, The Coq Development Team : The Coq proof assistant reference manual

D. Gallois-wong, S. Boldo, T. ;. Hilaire, W. M. Farmer, G. O. Passmore et al., A coq formalization of digital filters, Intelligent Computer Mathematics-11th International Conference, CICM 2018, vol.11006, pp.87-103, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01728828

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

, The Coq Development Team: The Coq Proof Assistant Reference Manual, 2017.

T. Hilaire, P. Chevrel, and J. Whidborne, A unifying framework for finite wordlength realizations, IEEE Trans. on Circuits and Systems, vol.8, issue.54, pp.1765-1774, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01317352

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

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A user-friendly library of real analysis for Coq, Mathematics in Computer Science, vol.9, issue.1, pp.41-62, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00860648

B. Akbarpour and S. Tahar, Error analysis of digital filters using hol theorem proving, from the 4th International Workshop on Computational Models of Scientific Reasoning and Applications, vol.5, pp.651-666, 2007.

B. Akbarpour, S. Tahar, and A. Dekdouk, Formalization of fixed-point arithmetic in HOL, Formal Methods in System Design, vol.27, issue.1, pp.173-200, 2005.

J. Park, M. Pajic, O. Sokolsky, and I. Lee, Automatic Verification of Finite Precision Implementations of Linear Controllers, pp.153-169, 2017.

B. Lopez, Implémentation optimale de filtres linéaires en arithmétique virgule fixe, 2014.

T. Hilaire, A. Volkova, and M. Ravoson, Reliable fixed-point implementation of linear data-flows, Proc. IEEE Workshop on Signal Processing Systems (SiPS), 2016.
URL : https://hal.archives-ouvertes.fr/hal-01347637

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, 4th Conference on Interactive Theorem Proving, vol.7998, pp.163-179, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00816699

S. Boldo and G. Melquiond, Computer Arithmetic and Formal Proofs, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01632617

N. Damouche, M. Martel, and A. Chapoutot, Improving the numerical accuracy of programs by automatic transformation, International Journal on Software Tools for Technology Transfer, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01373666

S. The-alt-ergo and . Solver, , 2018.

J. Baril, R. Genestier, A. Giorgetti, and A. Petrossian, Rooted planar maps modulo some patterns, Discrete Mathematics, vol.339, issue.4, pp.1199-1205, 2016.
URL : https://hal.archives-ouvertes.fr/hal-02131164

J. Baril and V. Vajnovszki, A permutation code preserving a double Eulerian bistatistic, Discrete Applied Mathematics, vol.224, pp.9-15, 2017.

S. Berghofer and T. Nipkow, Random testing in Isabelle/HOL, SEFM'04, pp.230-239, 2004.

F. Bobot, J. Filliâtre, C. Marché, G. Melquiond, and A. Paskevich, The Why3 Platform, 2018.
URL : https://hal.archives-ouvertes.fr/hal-00822856

J. Bowles and M. B. Caminati, A verified algorithm enumerating event structures, CICM'17, vol.10383, pp.239-254, 2017.

M. Carlier, C. Dubois, and A. Gotlieb, Constraint reasoning in FOCALTEST, Proceedings of the 5th International Conference on Software and Data Technologies, vol.2, pp.82-91, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00699233

K. Claessen and J. Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, vol.35, pp.268-279, 2000.

M. Clochard, J. Filliâtre, C. Marché, and A. Paskevich, Formalizing semantics with an automatic program verifier, VSTTE'14, vol.8471, pp.37-51, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01067197

, The Coq Development Team. The Coq Proof Assistant Reference Manual

S. Cruanes, Satisfiability modulo bounded checking, Automated Deduction-CADE 26, vol.10395, pp.114-129, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01572531

. The, , 2018.

L. De-moura and N. Björner, Z3: An efficient SMT solver, TACAS'08, vol.4963, pp.337-340, 2008.

C. Dubois and A. Giorgetti, Tests and proofs for custom data generators. Formal Aspects of Computing, 2018.

C. Dubois, A. Giorgetti, and R. Genestier, Tests and proofs for enumerative combinatorics, TAP'16, vol.6792, pp.57-75, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01670709

D. Dumont and G. Viennot, A combinatorial interpretation of the Seidel generation of Genocchi numbers, Combinatorial Mathematics, Optimal Designs and Their Applications, vol.6, pp.77-87, 1980.

P. Dybjer, Q. Haiyan, and M. Takeyama, Combining testing and proving in dependent type theory, TPHOLs'03, vol.2758, pp.188-203, 2003.

J. Filliâtre and M. Pereira, Itérer avec confiance, JFLA'16, 2016.

J. Filliâtre and M. Pereira, A modular way to reason about iteration, NFM'16, vol.9690, pp.322-336, 2016.

R. Genestier, Vérification formelle de programmes de génération de données structurées, 2016.

R. Genestier, A. Giorgetti, and G. Petiot, Gagnez sur tous les tableaux, JFLA'15, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01099135

R. Genestier, A. Giorgetti, and G. Petiot, Sequential generation of structured arrays and its deductive verification, TAP'15, vol.9154, pp.109-128, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01228995

A. Giorgetti and R. Lazarini, Preuve de programmes d'´ enumération avec Why3, AFADL'18, pp.14-19, 2018.

A. Giorgetti and V. Senni, Specification and Validation of Algorithms Generating Planar Lehman Words, GASCom', vol.12, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00753008

G. Gonthier, The four colour theorem: Engineering of a formal proof, ASCM'07, vol.5081, pp.333-333, 2008.

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A machinechecked proof of the odd order theorem, ITP'13, pp.163-179, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00816699

D. Jackson and C. Damon, Elements of style: Analyzing a software design feature with a counterexample detector, IEEE Trans. Softw. Eng, vol.22, issue.7, pp.484-495, 1996.

C. Laisant, Sur la numération factorielle, application aux permutations, pp.176-183, 1888.

L. Lampropoulos, D. Gallois-wong, C. Hrit¸cuhrit¸cu, J. Hughes, B. C. Pierce et al., Beginner's luck: a language for property-based generators, POPL'17, pp.114-129, 2017.

D. H. Lehmer, Teaching combinatorial tricks to a computer, In Proc. Sympos. Appl. Math. Combinatorial Analysis, vol.10, pp.179-193, 1960.

R. Mantaci and F. Rakotondrajao, A permutations representation that knows what, Eulerian" means. Discrete Mathematics and Theoretical Computer Science, vol.4, issue.2, pp.101-108, 2001.
URL : https://hal.archives-ouvertes.fr/hal-00958950

S. Owre, Random testing in PVS, Workshop on Automated Formal Methods (AFM), 2006.

Z. Paraskevopoulou, C. Hrit¸cuhrit¸cu, M. Dénès, L. Lampropoulos, and B. C. Pierce, Foundational property-based testing, ITP'15, vol.9236, pp.325-343, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01162898

V. Vajnovszki, Lehmer code transforms and Mahonian statistics on permutations. Discrete Mathematics, vol.313, pp.581-589, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00824066

, Axiomes de Continuité en Géométrie Neutre : une Étude Mécanisée en Coq Gries

, Disponibilité Le développement Coq décrit dans cet article est disponible dans la bibliothèque GeoCoq

R. Baldus, Zur Axiomatik der Geometrie. I : Über Hilberts Vollständigkeitsaxiom, Mathematische Annalen, vol.100, issue.1, pp.321-333, 1928.
DOI : 10.1007/bf01448848

R. Baldus, Zur Axiomatik der Geometrie. III : Über das Archimedische und das Cantorsche Axiom, Sitzungsberichte Heidelberg, vol.5, issue.12, 1930.
DOI : 10.1007/bf01448848

G. Braun, P. Boutry, and J. Narboux, From Hilbert to Tarski, Eleventh International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2016, p.19, 2016.
DOI : 10.1007/978-3-642-40672-0_7
URL : https://hal.archives-ouvertes.fr/hal-01332044

P. Boutry, G. Braun, and J. Narboux, Formalization of the Arithmetization of Euclidean Plane Geometry and Applications, Journal of Symbolic Computation, vol.98, pp.149-168, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01483457

M. Beeson, Proof and Computation in Geometry, Automated Deduction in Geometry (ADG 2012, vol.7993, pp.1-30, 2013.
DOI : 10.1007/978-3-642-40672-0_1
URL : http://www.michaelbeeson.com/research/papers/Edinburgh.pdf

P. Boutry, C. Gries, J. Narboux, and P. Schreck, Parallel postulates and continuity axioms : a mechanized study in intuitionistic logic using Coq, Journal of Automated Reasoning, p.68, 2017.
DOI : 10.1007/s10817-017-9422-8
URL : https://hal.archives-ouvertes.fr/hal-01178236

G. Braun and J. Narboux, From Tarski to Hilbert, Post-proceedings of Automated Deduction in Geometry, vol.7993, pp.89-109, 2012.
DOI : 10.1007/978-3-642-40672-0_7
URL : https://hal.archives-ouvertes.fr/hal-01332044

P. Boutry, J. Narboux, P. Schreck, and G. Braun, A short note about case distinctions in Tarski's geometry, Proceedings of the 10th Int. Workshop on Automated Deduction in Geometry, pp.51-65, 2014.

G. Cantor, Uber eine Eigenschaft des Inbegriffs aller reellen algebraischen Zahlen. Journal für die reine und angewandte Mathematik, vol.77, pp.258-262, 1874.
DOI : 10.1007/978-3-7091-9516-1_2

M. Dehn, Die Legendre'schen Sätze über die Winkelsumme im Dreieck, Mathematische Annalen, vol.53, issue.3, pp.404-439, 1900.
DOI : 10.1007/bf01448980
URL : https://zenodo.org/record/2520561/files/article.pdf

J. Duprat, Fondements de géométrie euclidienne, 2010.

P. Ehrlich, From Completeness to Archimedean Completeness : An Essay in the Foundations of Euclidean Geometry, A Symposium on David Hilbert, vol.110, pp.57-76, 1997.

P. Ehrlich, The Rise of non-Archimedean Mathematics and the Roots of a Misconception I : The Emergence of non-Archimedean Systems of Magnitudes. Archive for History of Exact Sciences, vol.60, pp.1-121, 2006.

C. Gries, P. Boutry, and J. Narboux, Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq, Les vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Actes des Vingt-septièmes Journées Francophones des Langages Applicatifs, p.15, 2016.

E. Giovannini, Completitud y continuidad en Fundamentos de la Geometría de Hilbert : acerca del Vollständigkeitsaxiom, History and Foundations of Science, vol.28, pp.139-163, 2013.
DOI : 10.1387/theoria.4544
URL : http://www.ehu.eus/ojs/index.php/THEORIA/article/download/4544/7041

M. Greenberg, Aristotle's axiom in the foundations of geometry, Journal of Geometry, vol.33, issue.1, pp.53-57, 1988.

, Axiomes de Continuité en Géométrie Neutre : une Étude Mécanisée en Coq Gries

M. J. Greenberg, Old and New Results in the Foundations of Elementary Plane Euclidean and Non-Euclidean Geometries, The American Mathematical Monthly, vol.117, issue.3, pp.198-219, 2010.

. Haragauri-narayan-gupta, Contributions to the axiomatic foundations of geometry, 1965.

J. Hall, Completeness of ordered fields, p.2011, 2011.

R. Hartshorne, Geometry : Euclid and beyond. Undergraduate texts in mathematics, 2000.

D. Hilbert, Grundlagen der Geometrie. Leipzig, p.1899

D. Hilbert, Foundations of Geometry, 1977.

G. E. Martin, The Foundations of Geometry and the Non-Euclidean Plane, Undergraduate Texts in Mathematics, 1998.

. Victor-pambuccian, The elementary Archimedean axiom in absolute geometry, 2018.

M. Pasch, Vorlesungen über neuere Geometrie, p.1882

F. Rothe, Several Topics from Geometry. unpublished, 2014.

W. Schwabhäuser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie, 1983.

J. Strommer, Über die Kreisaxiome, Periodica Mathematica Hungarica, vol.4, pp.3-16, 1973.

A. Tarski, A decision method for elementary algebra and geometry, 1951.

W. Weber, Über die Widersprüche in gewissen linearen Vollständigkeitsaxiomen der Geometrie, Sitzungsber. Preuß. Akad. Wiss., Phys.-Math. Kl, pp.376-382, 1938.

A. Abel, Mathematical Structures in Computer Science, 2008.

S. Colin, Specifying the unboxability check on mutually recursive datatypes in OCaml, 2018.

J. Garrigue, Relaxing the value restriction, FLOPS, 2004.

R. Lepigre and C. Raffalli, Abstract representation of binders in ocaml using the bindlib library, LFMTP, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01972050

X. Leroy, Efficient data representation in polymorphic languages, PLILP, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00075295

X. Leroy, Unboxed objects and polymorphic typing, POPL, 1992.
URL : https://hal.archives-ouvertes.fr/hal-01499973

J. Peterson, Untagged data in tagged environments: Choosing optimal representations at compile time, FPCA, 1989.

L. Simon, P. Jones, and J. Launchbury, Unboxed values as first class citizens in a nonstrict functional language, FPCA, 1991.

G. Scherer and D. Rémy, Gadts meet subtyping, ESOP, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00772993

V. Simonet and F. Pottier, A constraint-based approach to guarded algebraic data types. TOPLAS, Interactive Theorem Proving, pp.20-39, 2007.

P. Henk and . Barendregt, Introduction to generalized type systems, Journal of Functional Programming, vol.1, issue.2, pp.121-154, 1991.

B. Barras and B. Bernardo, Implicit calculus of constructions as a programming language with dependent types, Conference on Foundations of Software Science and Computation Structures, vol.4962, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00429543

A. Bove, P. Dybjer, and U. Norell, A brief overview of Agda-a functional language with dependent types, International Conference on Theorem Proving in Higher-Order Logics, vol.5674, pp.73-78, 2009.

B. Bernardo, Towards an implicit calculus of inductive constructions. extending the implicit calculus of constructions with union and subset types, International Conference on Theorem Proving in Higher-Order Logics, vol.5674, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00432649

J. Bernardy, P. Jansson, and R. Paterson, Proofs for free: Parametricity for dependent types, Journal of Functional Programming, vol.22, issue.2, pp.1-46, 2012.

E. Brady, Idris, a general-purpose dependently typed programming language: Design and implementation, Journal of Functional Programming, vol.23, issue.5, pp.552-593, 2013.

E. Burmako, Scala macros: let our powers combine!: on how rich syntax and static types work with metaprogramming, Workshop on Scala, vol.3, pp.1-3, 2013.

J. Cockx and A. Abel, Elaborating dependent (co)pattern matching, Proceedings of the ACM on Programming Languages, vol.2, 2018.

D. Christiansen and E. Brady, Elaborator reflection: Extending Idris in Idris, International Conference on Functional Programming, pp.284-297, 2016.

A. Chlipala, Certified Programming with Dependent Types, 2013.

N. Anders-danielsson and U. Norell, Parsing mixfix operators, Implementation and Application of Functional Languages, vol.6836, pp.80-99, 2008.

. Daniel-de-rauglaudre, Camlp4 reference manual, 2003.

R. W. Floyd, Syntactic analysis and operator precedence, Journal of the ACM, vol.10, issue.3, pp.316-333, 1963.

E. Giménez, Codifying guarded definitions with recursive schemes, 1994.

P. Gérard, C. Huet, and . Paulin-mohring, The Coq proof assistant reference manual, 2000.

G. Malecha, Extensible Proof Engineering in Intensional Type Theory, 2014.

N. Mishra, -. Linger, and T. Sheard, Erasure and polymorphism in pure type systems, Conference on Foundations of Software Science and Computation Structures, vol.4962, pp.350-364, 2008.

F. Mccabe and M. Sperber, Feel different on the Java platform: The Star programming language, International Conference on Principles and Practices of Programming on the Java Platform, pp.89-100, 2013.

F. Pfenning and C. Schürmann, System description: Twelf-a meta-logical framework for deductive systems, International Conference on Automated Deduction, vol.1632, pp.202-206, 1999.

C. Benjamin, D. M. Pierce, and . Turner, Local type inference. Transactions on Programming Languages and Systems, vol.22, pp.1-44, 2000.

J. Rafkind and M. Flatt, Honu: A syntactically extensible language, Proceedings of Generative Programming and Component Engineering, 2012.

N. Swamy, C. Hrit¸cuhrit¸cu, A. Keller, A. Rastogi, S. Delignat-lavaud et al., Dependent types and multi-monadic effects in F*, Symposium on Principles of Programming Languages, pp.256-270, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01265793

T. Sheard and S. , Template metaprogramming for Haskell, Haskell Workshop, pp.1-16, 2002.

T. Sheard and E. Pa?ali´pa?ali´c, Meta-programming with built-in type equality, Logical Frameworks and Meta-Languages, 2004.

, Pour l'analyse par interprétation abstraite (EVA), le portage a un impact positif, soit en réduisant le nombre d'alarmes du code C commun, soit en améliorant la précision, soit encore en mettant au jour de nouvelles alarmes mémoire du code porté

D. Andriesse, X. Chen, V. Van-der-veen, A. Slowinska, and H. Bos, An In-Depth Analysis of Disassembly on Full-Scale x86/x64 Binaries, 25th USENIX Security Symposium, USENIX Security 16, pp.583-600, 2016.

G. Balakrishnan and T. W. Reps, WYSINWYX : what you see is not what you execute, ACM Trans. Program. Lang. Syst, vol.32, issue.6, 2010.

T. Ball, E. Bounimova, V. Levin, R. Kumar, and J. Lichtenberg, The static driver verifier research platform, Computer Aided Verification, 22nd International Conference, CAV 2010, vol.6174, pp.119-122, 2010.

S. Bardin, P. Herrmann, J. Leroux, O. Ly, R. Tabary et al., The BINCOA Framework for Binary Code Analysis, Computer Aided Verification De l'Assembleur sur la Ligne ? Appelez TInA ! Recoules, vol.6806, pp.165-170, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01006499

S. Bardin, P. Herrmann, and F. Védrine, Refinement-Based CFG Reconstruction from Unstructured Programs, Verification, Model Checking, and Abstract Interpretation-12th International Conference, vol.6538, pp.54-69, 2011.

C. Barrett and C. Tinelli, Satisfiability modulo theories, Handbook of Model Checking, pp.305-343, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01095009

P. Baudin, F. Bobot, L. Correnson, and Z. Dargaye, WP Manual, Frama-C Chlorine-20180501 edition, 2018.

S. Blazy, B. Robillard, and A. W. Appel, Formal Verification of Coalescing Graph-Coloring Register Allocation, Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, vol.6012, pp.145-164, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00477689

D. Brumley, I. Jager, T. Avgerinos, and E. J. Schwartz, BAP : A Binary Analysis Platform, pp.463-469, 2011.

D. Brumley, J. Lee, E. J. Schwartz, and M. Woo, Native x86 Decompilation Using SemanticsPreserving Structural Analysis and Iterative Control-Flow Structuring, Proceedings of the 22th USENIX Security Symposium, pp.353-368, 2013.

D. Bühler, Structuring an Abstract Interpreter through Value and State Abstractions:EVA, an Evolved Value Analysis for Frama-C, 2017.

C. Cadar, D. Dunbar, D. R. Engler, and . Klee, Unassisted and Automatic Generation of HighCoverage Tests for Complex Systems Programs, 8th USENIX Symposium on Operating Systems Design and Implementation, pp.209-224, 2008.

N. Carvalho, C. Da-silva, J. S. Sousa, A. Pinto, and . Tomb, Formal Verification of kLIBC with the WP Frama-C Plug-in, NASA Formal Methods-6th International Symposium, NFM 2014, vol.8430, pp.343-358, 2014.

B. E. Chang, M. Harren, and G. C. Necula, Analysis of Low-Level Code Using Cooperating Decompilers, pp.318-335, 2006.

C. Cifuentes, Interprocedural data flow decompilation, J. Prog. Lang, vol.4, issue.2, pp.77-99, 1996.

C. Cifuentes and K. J. Gough, Decompilation of Binary Programs, Softw., Pract. Exper, vol.25, issue.7, pp.811-829, 1995.

C. Cifuentes, D. Simon, and A. Fraboulet, Assembly to High-Level Language Translation, 1998 International Conference on Software Maintenance, ICSM, pp.228-237, 1998.
URL : https://hal.archives-ouvertes.fr/hal-00399650

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal et al., VCC : A Practical System for Verifying Concurrent C, pp.23-42, 2009.

N. Corteggiani, G. Camurati, and A. Francillon, Inception : System-Wide Security Testing of Real-World Embedded Systems Software, 27th USENIX Security Symposium, USENIX Security, pp.309-326, 2018.

P. Cousot and R. Cousot, Abstract Interpretation : A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pp.238-252, 1977.

P. Cousot and R. Cousot, Abstract interpretation : past, present and future, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, vol.2, pp.1-2, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01108790

D. Delmas and J. Souyris, Astrée : From Research to Industry, Static Analysis, 14th International Symposium, vol.4634, pp.437-451, 2007.

. Springer, , 2007.

A. Djoudi and S. Bardin, BINSEC : Binary Code Analysis with Low-Level Regions, pp.212-217, 2015.
URL : https://hal.archives-ouvertes.fr/cea-01834975

A. Djoudi, S. Bardin, and É. Goubault, Recovering High-Level Conditions from Binary Programs, pp.235-253, 2016.
URL : https://hal.archives-ouvertes.fr/cea-01834972

, DWARF Debugging Information Format Committee. DWARF Debugging Information Format, vol.5, 2017.

A. Fehnker, R. Huuck, F. Rauch, and S. Seefried, Some Assembly Required-Program Analysis of Embedded System Code, Eighth IEEE International Working Conference on Source Code Analysis and Manipulation, pp.15-24, 2008.

R. W. Floyd, Assigning meanings to programs, Proceedings of Symposia in Applied Mathematics 19, pp.19-32, 1967.

P. Godefroid, M. Y. Levin, and D. A. Molnar, SAGE : whitebox fuzzing for security testing, Commun. ACM, vol.55, issue.3, pp.40-44, 2012.

C. A. Hoare, An Axiomatic Basis for Computer Programming, Commun. ACM, vol.12, issue.10, pp.576-580, 1969.

, Intel Corporation. Intel ® 64 and IA-32 Architectures Software Developer's Manual, 2016.

S. Kim, M. Faerevaag, M. Jung, S. Jung, D. Oh et al., Testing intermediate representations for binary analysis, Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, pp.353-364, 2017.

J. Kinder and D. Kravchenko, Alternating Control Flow Reconstruction, Verification, Model Checking, and Abstract Interpretation-13th International Conference, VMCAI 2012, vol.7148, pp.267-282, 2012.

J. C. King, Symbolic Execution and Program Testing, Commun. ACM, vol.19, issue.7, pp.385-394, 1976.

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.
URL : https://hal.archives-ouvertes.fr/cea-01808981

J. Lee, T. Avgerinos, and D. Brumley, TIE : Principled Reverse Engineering of Types in Binary Programs, NDSS, 2011.

S. Maus, Verification of hypervisor subroutines written in Assembler (Verifikation von Hypervisorunterrutinen, geschrieben in Assembler), 2011.

S. Maus, M. Moskal, and W. Schulte, Vx86 : x86 Assembler Simulated in C Powered by Automated Theorem Proving, pp.284-298, 2008.

X. Meng and B. P. Miller, Binary code is not easy, Proceedings of the 25th International Symposium on Software Testing and Analysis, pp.24-35, 2016.

M. O. Myreen, M. J. Gordon, and K. Slind, Machine-Code Verification for Multiple Architectures-An Application of Decompilation into Logic, Formal Methods in Computer-Aided Design, pp.1-8, 2008.

G. C. Necula, Translation validation for an optimizing compiler, Mounier et Potet of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp.83-94, 2000.

P. W. O'hearn, From Categorical Logic to Facebook Engineering, 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, pp.17-20, 2015.

A. Reid, Trustworthy specifications of ARM® v8-A and v8-M system level architecture, Formal Methods in Computer-Aided Design, pp.161-168, 2016.

T. Reinbacher and J. Brauer, Precise control flow reconstruction using boolean logic, Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, part of the Seventh Embedded Systems Week, pp.117-126, 2011.

M. Rigger, S. Marr, S. Kell, D. Leopoldseder, and H. Mössenböck, An Analysis of x86-64 Inline Assembly in C Programs, Proceedings of the 14th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments, pp.84-99, 2018.

X. , Certification of compiled assembly code by invariant translation, STTT, vol.6, issue.1, pp.15-37, 2004.

E. Robbins, A. King, and T. Schrijvers, From MinX to MinC : Semantics-driven Decompilation of Recursive Datatypes, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pp.191-203, 2016.

S. Schmaltz and A. Shadrin, Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT, pp.18-33, 2012.

E. Schulte, J. Ruchti, M. Noonan, D. Ciarletta, and A. Logino, Evolving Exact Decompilation, BAR 2018, Workshop on Binary Analysis Research, 2018.

A. Sepp, B. Mihaila, and A. Simon, Precise Static Analysis of Binaries by Extracting Relational Information, 18th Working Conference on Reverse Engineering, pp.357-366, 2011.

T. A. Sewell, M. O. Myreen, and G. Klein, Translation validation for a verified OS kernel, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, pp.471-482, 2013.

Y. Shoshitaishvili, R. Wang, C. Salls, N. Stephens, M. Polino et al., SoK : (State of) The Art of War : Offensive Techniques in Binary Analysis, IEEE Symposium on Security and Privacy, 2016.

, The High Performance Editor for the Web, ACE

. Learn-ocaml,

. Learn-ocaml-autogen,

B. Canou, R. D. Cosmo, and G. Henry, Scaling Up Functional Programming Education : Under the Hood of the OCaml MOOC, PACML, vol.1, 2017.

D. Merkel, Docker : Lightweight Linux Containers for Consistent Development and Deployment, Linux J, issue.239, 2014.

M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Certified Programs and Proofs-First International Conference, vol.7086, pp.135-150, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00639130

F. Bacchus, X. Chen, P. Van-beek, and T. Walsh, Binary vs. non-binary constraints, Artificial Intelligence, vol.140, issue.1, pp.1-37, 2002.

, Formally Verified Decomposition of Non-binary Constraints into Equivalent Binary Constraints C

C. Bessiere, E. Hebrard, G. Katsirelos, Z. Kiziltan, N. Narodytska et al., Reasoning about Constraint Models, PRICAI 2014: Trends in Artificial Intelligence-13th Pacific Rim Int. Conference on Artificial Intelligence, vol.8862, pp.795-808, 2014.
URL : https://hal.archives-ouvertes.fr/lirmm-01228300

M. Cadoli and T. Mancini, Using a Theorem Prover for Reasoning on Constraint Problems, Applied Artificial Intelligence, vol.21, issue.4&5, pp.383-404, 2007.

M. Carlier, C. Dubois, and A. Gotlieb, A Certified Constraint Solver over Finite Domains, Formal Methods (FM), vol.7436, pp.116-131, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126135

M. Carlier, C. Dubois, and A. Gotlieb, A First Step in the Design of a Formally Verified ConstraintBased Testing Tool: Focaltest, Tests and Proofs-TAP 2012, vol.7305, pp.35-50, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126115

L. Cruz-filipe, M. J. Heule, W. A. Hunt, M. Kaufmann, and P. Schneider-kamp, Efficient Certified RAT Verification, Automated Deduction-CADE 26-26th International Conference on Automated Deduction, vol.10395, pp.220-236, 2017.

J. Esparza, P. Lammich, R. Neumann, T. Nipkow, A. Schimpf et al., A Fully Verified Executable LTL Model Checker, Computer Aided Verification, vol.8044, pp.463-478, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01226469

M. Fleury, J. C. Blanchette, and P. Lammich, A verified SAT solver with watched literals using imperative HOL, 7th ACM SIGPLAN Int. Conference on Certified Programs and Proofs, pp.158-171, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01904647

O. Grinchtein, M. Carlsson, C. Dubois, and J. Pearson, Exploring Properties of a Telecommunication Protocol with Message Delay using an Interactive Theorem Prover, SEFM 2018, vol.10886, pp.239-253

S. Lescuyer and S. Conchon, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, FroCos, vol.5749, pp.287-303, 2009.

A. Mackworth, Consistency in Networks of Relations, Art. Intel, vol.8, issue.1, pp.99-118, 1977.

F. Maric, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Theor. Comput. Sci, vol.411, issue.50, pp.4333-4356, 2010.

R. Neumann, Using Promela in a Fully Verified executable LTL Model Checker, Verified Software: Theories, Tools and Experiments, vol.8471, pp.105-114, 2014.

F. Rossi, C. J. Petrie, and V. Dhar, On the Equivalence of Constraint Satisfaction Problems, ECAI, pp.550-556, 1990.

N. Shankar and M. Vaucher, The Mechanical Verification of a DPLL-based Satisfiability Solver, Electr. Notes Theor. Comput. Sci, vol.269, pp.3-17, 2011.

M. Spasic and F. Maric, Formalization of Incremental Simplex Algorithm by Stepwise Refinement, FM 2012: Formal Methods-18th Int. Symposium, vol.7436, pp.434-449, 2012.

K. Stergiou and T. Walsh, Encodings of Non-Binary Constraint Satisfaction Problems, Sixteenth National Conference on Artificial Intelligence and Eleventh Conference on Innovative Applications of Artificial Intelligence, pp.163-168, 1999.

M. Veksler and O. Strichman, A Proof-producing CSP Solver, Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, 2010.

B. Exécution-symbolique-robuste, S. Farinier, R. Bardin, and M. Bonichon, Potet-Initialisation de la mémoire à celle observée à l'exécution (concrétisation) : là encore on enlève certains faux positifs (une partie de ces valeurs est effectivement constante d'une exécution à l'autre), mais pas tous (certaines valeurs ne sont pas constantes d'une exécution à l'autre) ; par ailleurs la contrainte induite peut devenir trop imposante pour être gérée par les solveurs. 'outil Binsec. Le point (2) est évidemment un problème puisqu'il repose sur l'utilisateur. Comme expliqué précédemment, notre technique ne peut pas produire de faux positifs quand « trop » d'entrées sont déclarées non contrôlées

C. Barrett and C. Tinelli, Satisfiability modulo theories, Handbook of Model Checking, pp.305-343, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01095009

C. Cadar, D. Dunbar, and D. R. Engler, KLEE : Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs, 8th USENIX Symposium on Operating Systems Design and Implementation, pp.209-224, 2008.

C. Cadar and K. Sen, Symbolic execution for software testing : three decades later, Commun. ACM, vol.56, issue.2, pp.82-90, 2013.

V. Chipounov, V. Kuznetsov, and G. Candea, S2E : a platform for in-vivo multi-path analysis of software systems, Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, pp.265-278, 2011.

R. David, S. Bardin, T. D. Ta, L. Mounier, J. Feist et al., BINSEC/SE : A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis, SANER, pp.653-656, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01721502

A. Djoudi and S. Bardin, BINSEC : Binary Code Analysis with Low-Level Regions, Tools and Algorithms for the Construction and Analysis of Systems-21st International Conference, TACAS 2015, pp.212-217, 2015.
URL : https://hal.archives-ouvertes.fr/cea-01834975

B. Farinier, S. Bardin, R. Bonichon, and M. Potet, Model generation for quantified formulas : A taint-based approach, 30th International Conference on Computer Aided Verification (CAV 2018), 2018.
URL : https://hal.archives-ouvertes.fr/cea-01709306

B. Farinier, R. David, S. Bardin, and M. Lemerre, Arrays made simpler : An efficient, scalable and thorough preprocessing, 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2018), 2018.

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

, Un Mécanisme de Preuve par Réflexion pour Why3 et son Application aux, Algorithmes de GMP Raphaël Rieu-Helft, vol.1, issue.2

. Trustinsoft,

U. Inria and . Paris-saclay,

, Résumé Nous présentons un mécanisme de preuves par réflexion pour la plateforme de vérification Why3. L'utilisateur peut facilement écrire des procédures de décision dédiées, formellement vérifiées et qui utilisent pleinement les fonctionnalités impératives du langage WhyML. L'impact sur la base de confiance est minimal

, Un Mécanisme de Preuve par Réflexion pour Why3 R. Rieu-Helft

, Traditionnellement, les preuves par réflexion se font en évaluant des termes purs présents dans des propositions logiques. Cependant, le langage de programmation fourni par Why3 est beaucoup plus riche : variables mutables, tableaux, exceptions, boucles

, Étant capables d'écrire des procédures de décision en WhyML, de les vérifier avec Why3, vol.11

, Preuves par réflexion Le principe général de la preuve par réflexion est le suivant. Notons P la proposition que l'on le calcul, il s'agit d'une procédure de preuve par réflexion, Cette approche a été utilisée dans de nombreux contextes

, Notons cependant que si n'est pas exprimable dans le langage logique, son inverse l'est. tactique Coq quote, avec quelques améliorations : la fonction d'interprétation peut être plus complexe, elle supporte les quantificateurs, le contexte logique peut être réifié, et l'utilisateur n'a pas besoin de spécifier quels termes peuvent être des constantes, Réification Une difficulté est que la fonction n'est pas exprimable dans le langage logique, et que du système

R. Rieu-helft,

. Références,

F. Besson, Fast reflexive arithmetic tactics the linear case and beyond, International Workshop on Types for Proofs and Programs, vol.4502, pp.48-62, 2007.
DOI : 10.1007/978-3-540-74464-1_4

R. William-blanc, E. Kneuss, V. Kuncak, and P. Suter, An overview of the Leon verification system: Verification by translation to recursive functions, 4th Annual Scala Workshop, 2013.

A. Chaieb and T. Nipkow, Proof synthesis and reflection for linear arithmetic, Journal of Automated Reasoning, vol.41, issue.1, pp.33-59, 2008.
DOI : 10.1007/s10817-008-9101-x

G. Claret, L. Del-carmen-gonzález, Y. Huesca, B. Régis-gianas, and . Ziliani, Lightweight proof by reflection using a posteriori simulation of effectful computation, 4th International Conference on Interactive Theorem Proving, vol.7998, pp.67-83, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00870110

M. Clochard, Preuves taillées en biseau, Vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), 2017.

M. Clochard, L. Gondelman, and M. Pereira, The Matrix reproved, Journal of Automated Reasoning, vol.60, issue.3, pp.365-383, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01316902

J. , C. Filliâtre, and A. Paskevich, Why3-where programs meet provers, 22nd European Symposium on Programming, vol.7792, pp.125-128, 2013.

B. Grégoire and A. Mahboubi, Proving equalities in a commutative ring done right in Coq, 18th International Conference on Theorem Proving in Higher Order Logics, pp.98-113, 2005.

J. Harrison, Metatheory and reflection in theorem proving: A survey and critique, 1995.

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

G. Melquiond and R. Rieu-helft, A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms, 9th International Joint Conference on Automated Reasoning, number 10900 in Lecture Notes in Computer Science, pp.178-193, 2018.

N. Moller and T. Granlund, Improved division by invariant integers, IEEE Transactions on Computers, vol.60, issue.2, pp.165-175, 2011.
DOI : 10.1109/tc.2010.143

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, vol.10712, pp.84-101, 2017.
DOI : 10.1007/978-3-319-72308-2_6
URL : https://hal.archives-ouvertes.fr/hal-01519732