Bibliography

Major publications by the team in recent years

• 1V. Benzaken, É. Contejean, S. Dumbrava.
  
  A Coq Formalization of the Relational Data Model, in: European Symposium on Programming, LNCS 8410, Grenoble, Z. Shao (editor), Lecture Notes in Computer Science, Springer, April 2014, pp. 189-208.
  
  http://hal.inria.fr/hal-00924156
• 2J. C. Blanchette, A. Paskevich.
  
  TFF1: The TPTP typed first-order form with rank-1 polymorphism, in: 24th International Conference on Automated Deduction (CADE-24), Lake Placid, USA, Lecture Notes in Artificial Intelligence, Springer, June 2013, vol. 7898.
  
  http://hal.inria.fr/hal-00825086
• 3F. Bobot, S. Conchon, É. Contejean, M. Iguernelala, A. Mahboubi, A. Mebsout, G. Melquiond.
  
  A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic, in: IJCAR 2012: Proceedings of the 6th International Joint Conference on Automated Reasoning, Manchester, UK, B. Gramlich, D. Miller, U. Sattler (editors), Lecture Notes in Computer Science, Springer, June 2012, vol. 7364, pp. 67–81.
  
  http://hal.inria.fr/hal-00687640
• 4F. Bobot, J.-C. Filliâtre, C. Marché, A. Paskevich.
  
  Why3: Shepherd Your Herd of Provers, in: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wrocław, Poland, August 2011, pp. 53–64.
  
  http://hal.inria.fr/hal-00790310
• 5S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, P. Weis.
  
  Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program, in: Journal of Automated Reasoning, April 2013, vol. 50, n^o 4, pp. 423–456.
  
  http://hal.inria.fr/hal-00649240/en/
• 6S. Boldo, G. Melquiond.
  
  Flocq: A Unified Library for Proving Floating-point Algorithms in Coq, in: Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Tübingen, Germany, E. Antelo, D. Hough, P. Ienne (editors), 2011, pp. 243–252.
  
  http://hal.archives-ouvertes.fr/inria-00534854/
• 7A. Charguéraud.
  
  Pretty-Big-Step Semantics, in: Proceedings of the 22nd European Symposium on Programming, M. Felleisen, P. Gardner (editors), Lecture Notes in Computer Science, Springer, March 2013, vol. 7792, pp. 41–60.
  
  http://hal.inria.fr/hal-00798227
• 8S. Conchon, A. Goel, S. Krstić, A. Mebsout, F. Zaïdi.
  
  Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems, in: CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification, Berkeley, California, USA, M. Parthasarathy, S. A. Seshia (editors), Lecture Notes in Computer Science, Springer, July 2012, vol. 7358.
  
  http://hal.archives-ouvertes.fr/hal-00799272
• 9J.-C. Filliâtre, L. Gondelman, A. Paskevich.
  
  The Spirit of Ghost Code, in: 26th International Conference on Computer Aided Verification, Vienna, Austria, A. Biere, R. Bloem (editors), Lecture Notes in Computer Science, Springer, July 2014, vol. 8859, pp. 1–16.
  
  http://hal.archives-ouvertes.fr/hal-00873187/en/
• 10G. Melquiond.
  
  Proving bounds on real-valued functions with computations, in: Proceedings of the 4th International Joint Conference on Automated Reasoning, Sydney, Australia, A. Armando, P. Baumgartner, G. Dowek (editors), Lecture Notes in Artificial Intelligence, 2008, vol. 5195, pp. 2–17.

Publications of the year

Doctoral Dissertations and Habilitation Theses

• 11C. Lelay.
  
  Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis, Université Paris Sud - Paris XI, June 2015.
  
  https://tel.archives-ouvertes.fr/tel-01228517

Articles in International Peer-Reviewed Journals

• 12F. Bobot, J.-C. Filliâtre, C. Marché, A. Paskevich.
  
  Let's Verify This with Why3, in: Software Tools for Technology Transfer (STTT), 2015, vol. 17, n^o 6, pp. 709-727.
  
  https://hal.inria.fr/hal-00967132
• 13S. Boldo, J.-H. Jourdan, X. Leroy, G. Melquiond.
  
  Verified Compilation of Floating-Point Computations, in: Journal of Automated Reasoning, February 2015, vol. 54, n^o 2, pp. 135-163. [ DOI : 10.1007/s10817-014-9317-x ]
  
  https://hal.inria.fr/hal-00862689
• 14S. Boldo, C. Lelay, G. Melquiond.
  
  Coquelicot: A User-Friendly Library of Real Analysis for Coq, in: Mathematics in Computer Science, March 2015, vol. 9, n^o 1, pp. 41-62. [ DOI : 10.1007/s11786-014-0181-1 ]
  
  https://hal.inria.fr/hal-00860648
• 15A. Charguéraud.
  
  Improving Type Error Messages in OCaml, in: Electronic Proceedings in Theoretical Computer Science, December 2015, vol. 198, pp. 80-97. [ DOI : 10.4204/EPTCS.198.4 ]
  
  https://hal.inria.fr/hal-01245843
• 16C. Dross, S. Conchon, J. Kanig, A. Paskevich.
  
  Adding Decision Procedures to SMT Solvers using Axioms with Triggers, in: Journal of Automated Reasoning, 2016, accepted for publication.
  
  https://hal.archives-ouvertes.fr/hal-01221066
• 17C. Marché, J. Kanig.
  
  Bridging the Gap between Testing and Formal Verification in Ada Development, in: ERCIM News, January 2015, vol. 100, 2 p.
  
  https://hal.inria.fr/hal-01102242
• 18É. Martin-Dorel, G. Melquiond.
  
  Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq, in: Journal of Automated Reasoning, 2015. [ DOI : 10.1007/s10817-015-9350-4 ]
  
  https://hal.inria.fr/hal-01086460
• 19P. Roux.
  
  Formal Proofs of Rounding Error Bounds, in: Journal of Automated Reasoning, 2015, 23 p. [ DOI : 10.1007/s10817-015-9339-z ]
  
  https://hal.archives-ouvertes.fr/hal-01091189

International Conferences with Proceedings

• 20U. A. Acar, A. Charguéraud, M. Rainey.
  
  A Work-Efficient Algorithm for Parallel Unordered Depth-First Search, in: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, Austin, Texas, United States, November 2015. [ DOI : 10.1145/2807591.2807651 ]
  
  https://hal.inria.fr/hal-01245837
• 21S. Boldo.
  
  Formal Verification of Programs Computing the Floating-Point Average, in: 17th International Conference on Formal Engineering Methods, Paris, France, M. Butler, S. Conchon, F. Zaïdi (editors), Springer, November 2015, vol. 9407, pp. 17-32.
  
  https://hal.inria.fr/hal-01174892
• 22S. Boldo.
  
  Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number, in: Eighth International Workshop on Numerical Software Verification, Seattle, WA, United States, S. Bogomolov, M. Martel (editors), Electronic Notes in Theoretical Computer Science, April 2015, pp. 50–55.
  
  https://hal.inria.fr/hal-01148409
• 23A. Charguéraud.
  
  Higher-Order Representation Predicates in Separation Logic, in: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, Florida, United States, January 2016.
  
  https://hal.inria.fr/hal-01245865
• 24A. Charguéraud, F. Pottier.
  
  Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation, in: 6th International Conference on Interactive Theorem Proving (ITP), Nanjing, China, August 2015. [ DOI : 10.1007/978-3-319-22102-1_9 ]
  
  https://hal.inria.fr/hal-01245872

National Conferences with Proceedings

• 25M. Clochard, L. Gondelman.
  
  Double WP : Vers une preuve automatique d'un compilateur, in: Journées Francophones des Langages Applicatifs, Val d'Ajol, France, January 2015.
  
  https://hal.inria.fr/hal-01094488

Conferences without Proceedings

• 26J.-C. Filliâtre, M. Pereira.
  
  Itérer avec confiance, in: Journées Francophones des Langages Applicatifs, Saint-Malo, France, January 2016.
  
  https://hal.inria.fr/hal-01240891
• 27C. Lelay.
  
  How to express convergence for analysis in Coq, in: The 7th Coq Workshop, Sophia Antipolis, France, June 2015.
  
  https://hal.archives-ouvertes.fr/hal-01169321

Scientific Books (or Scientific Book chapters)

• 28C. Paulin-Mohring.
  
  Introduction to the Calculus of Inductive Constructions, in: All about Proofs, Proofs for All, B. W. Paleo, D. Delahaye (editors), Studies in Logic (Mathematical logic and foundations), College Publications, January 2015, vol. 55.
  
  https://hal.inria.fr/hal-01094195

Internal Reports

• 29U. A. Acar, A. Charguéraud, M. Rainey.
  
  Fast Parallel Graph-Search with Splittable and Catenable Frontiers, Inria, January 2015.
  
  https://hal.inria.fr/hal-01089125
• 30C. Dross, C. Fumex, J. Gerlach, C. Marché.
  
  High-Level Functional Properties of Bit-Level Programs: Formal Specifications and Automated Proofs, Inria Saclay, December 2015, n^o RR-8821, 52 p.
  
  https://hal.inria.fr/hal-01238376

Scientific Popularization

• 31T. Vieville, S. Boldo, F. Masseglia, P. Bernhard.
  
  « Structures : organisation, complexité, dynamique » des mot-clés au sens inattendu, April 2015, Article de vulgarisation sur pixees.fr.
  
  https://hal.inria.fr/hal-01238442

References in notes

• 32B. Beckert, R. Hähnle, P. H. Schmitt (editors)
  
  Verification of Object-Oriented Software: The KeY Approach, Lecture Notes in Computer Science, Springer, 2007, vol. 4334.
• 33U. A. Acar, A. Charguéraud, S. Muller, M. Rainey.
  
  Atomic Read-Modify-Write Operations are Unnecessary for Shared-Memory Work Stealing, HAL, September 2013.
  
  http://hal.inria.fr/hal-00910130
• 34U. A. Acar, A. Charguéraud, M. Rainey.
  
  Scheduling parallel programs by work stealing with private deques, in: Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming, PPoPP '13, ACM Press, February 2013, pp. 219-228.
  
  http://hal.inria.fr/hal-00863028
• 35U. A. Acar, A. Charguéraud, M. Rainey.
  
  Theory and Practice of Chunked Sequences, in: European Symposium on Algorithms, Wroclaw, Poland, A. Schulz, D. Wagner (editors), Springer, September 2014, vol. Lecture Notes in Computer Science, n^o 8737, pp. 25–36.
  
  https://hal.inria.fr/hal-01087245
• 36J. B. Almeida, M. Barbosa, J.-C. Filliâtre, J. S. Pinto, B. Vieira.
  
  CAOVerif: An Open-Source Deductive Verification Platform for Cryptographic Software Implementations, in: Science of Computer Programming, October 2012.
• 37A. Ayad, C. Marché.
  
  Multi-Prover Verification of Floating-Point Programs, in: Fifth International Joint Conference on Automated Reasoning, Edinburgh, Scotland, J. Giesl, R. Hähnle (editors), Lecture Notes in Artificial Intelligence, Springer, July 2010, vol. 6173, pp. 127–141.
  
  http://hal.inria.fr/inria-00534333
• 38D. Baelde, P. Courtieu, D. Gross-Amblard, C. Paulin-Mohring.
  
  Towards Provably Robust Watermarking, in: ITP 2012, Lecture Notes in Computer Science, August 2012, vol. 7406.
  
  http://hal.inria.fr/hal-00682398
• 39C. Barrett, C. Tinelli.
  
  CVC3, in: 19th International Conference on Computer Aided Verification, Berlin, Germany, W. Damm, H. Hermanns (editors), Lecture Notes in Computer Science, Springer, July 2007, vol. 4590, pp. 298–302.
• 40P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, V. Prevosto.
  
  ACSL: ANSI/ISO C Specification Language, version 1.4, 2009.
• 41P. Behm, P. Benoit, A. Faivre, J.-M. Meynadier.
  
  METEOR : A successful application of B in a large project, in: Proceedings of FM'99: World Congress on Formal Methods, J. M. Wing, J. Woodcock, J. Davies (editors), Lecture Notes in Computer Science (Springer-Verlag), Springer Verlag, September 1999, pp. 369–387.
• 42F. Bobot, S. Conchon, É. Contejean, M. Iguernelala, S. Lescuyer, A. Mebsout.
  
  The Alt-Ergo Automated Theorem Prover, 2008.
• 43F. Bobot, J.-C. Filliâtre.
  
  Separation Predicates: a Taste of Separation Logic in First-Order Logic, in: 14th International Conference on Formal Ingineering Methods (ICFEM), Kyoto, Japan, Lecture Notes in Computer Science, Springer, November 2012, vol. 7635.
  
  http://hal.inria.fr/hal-00825088
• 44F. Bobot, J.-C. Filliâtre, C. Marché, G. Melquiond, A. Paskevich.
  
  Preserving User Proofs Across Specification Changes, in: Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE), Atherton, USA, E. Cohen, A. Rybalchenko (editors), Lecture Notes in Computer Science, Springer, May 2013, vol. 8164, pp. 191–201.
  
  http://hal.inria.fr/hal-00875395
• 45F. Bobot, J.-C. Filliâtre, C. Marché, G. Melquiond, A. Paskevich.
  
  The Why3 platform, version 0.81, version 0.81, LRI, CNRS & Univ. Paris-Sud & Inria Saclay, March 2013.
  
  http://hal.inria.fr/hal-00822856/
• 46M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, G. Smith.
  
  A Trusted Mechanised JavaScript Specification, in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, USA, ACM Press, January 2014.
  
  http://hal.inria.fr/hal-00910135
• 47S. Boldo.
  
  How to Compute the Area of a Triangle: a Formal Revisit, in: Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013.
  
  http://hal.inria.fr/hal-00790071
• 48S. Boldo.
  
  Deductive Formal Verification: How To Make Your Floating-Point Programs Behave, Université Paris-Sud, October 2014, Thèse d'habilitation.
  
  https://hal.inria.fr/tel-01089643
• 49S. Boldo.
  
  Formal verification of tricky numerical computations, in: 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Würzburg, Germany, September 2014.
  
  https://hal.inria.fr/hal-01088692
• 50S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, P. Weis.
  
  Formal Proof of a Wave Equation Resolution Scheme: the Method Error, in: Proceedings of the First Interactive Theorem Proving Conference, Edinburgh, Scotland, M. Kaufmann, L. C. Paulson (editors), LNCS, Springer, July 2010, vol. 6172, pp. 147–162.
  
  http://hal.inria.fr/inria-00450789/
• 51S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, P. Weis.
  
  Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program, in: Computers and Mathematics with Applications, 2014, vol. 68, n^o 3, pp. 325–352.
  
  http://hal.inria.fr/hal-00769201
• 52S. Boldo, J.-C. Filliâtre, G. Melquiond.
  
  Combining Coq and Gappa for Certifying Floating-Point Programs, in: 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Grand Bend, Canada, Lecture Notes in Artificial Intelligence, Springer, July 2009, vol. 5625, pp. 59–74.
• 53S. Boldo, J.-H. Jourdan, X. Leroy, G. Melquiond.
  
  A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, in: Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013.
  
  http://hal.inria.fr/hal-00743090
• 54S. Boldo, C. Lelay, G. Melquiond.
  
  Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives, in: Proceedings of the Second International Conference on Certified Programs and Proofs, Kyoto, Japan, C. Hawblitzel, D. Miller (editors), Lecture Notes in Computer Science, December 2012, vol. 7679, pp. 289–304.
  
  http://hal.inria.fr/hal-00712938
• 55S. Boldo, C. Lelay, G. Melquiond.
  
  Formalization of Real Analysis: A Survey of Proof Assistants and Libraries, in: Mathematical Structures in Computer Science, 2014.
  
  http://hal.inria.fr/hal-00806920
• 56S. Boldo, C. Marché.
  
  Formal verification of numerical programs: from C annotated programs to mechanical proofs, in: Mathematics in Computer Science, 2011, vol. 5, pp. 377–393.
  
  http://hal.inria.fr/hal-00777605
• 57S. Boldo, T. M. T. Nguyen.
  
  Proofs of numerical programs when the compiler optimizes, in: Innovations in Systems and Software Engineering, 2011, vol. 7, pp. 151–160.
  
  http://hal.inria.fr/hal-00777639
• 58T. Bormer, M. Brockschmidt, D. Distefano, G. Ernst, J.-C. Filliâtre, R. Grigore, M. Huisman, V. Klebanov, C. Marché, R. Monahan, W. Mostowski, N. Polikarpova, C. Scheben, G. Schellhorn, B. Tofan, J. Tschannen, M. Ulbrich.
  
  The COST IC0701 Verification Competition 2011, in: Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2011, B. Beckert, F. Damiani, D. Gurov (editors), Lecture Notes in Computer Science, Springer, 2012, vol. 7421.
  
  http://hal.inria.fr/hal-00789525
• 59L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, E. Poll.
  
  An overview of JML tools and applications, in: International Journal on Software Tools for Technology Transfer (STTT), June 2005, vol. 7, n^o 3, pp. 212–232.
• 60R. Chapman, F. Schanda.
  
  Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK, in: Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, G. Klein, R. Gamboa (editors), Lecture Notes in Computer Science, Springer, 2014, vol. 8558, pp. 17–26.
• 61A. Charguéraud.
  
  Characteristic formulae for the verification of imperative programs, in: Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP), Tokyo, Japan, M. M. T. Chakravarty, Z. Hu, O. Danvy (editors), ACM, September 2011, pp. 418-430.
• 62M. Clochard.
  
  Automatically verified implementation of data structures based on AVL trees, in: 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Vienna, Austria, D. Giannakopoulou, D. Kroening (editors), Lecture Notes in Computer Science, Springer, July 2014, vol. 8471, pp. 167–180.
  
  http://hal.inria.fr/hal-01067217
• 63M. Clochard, J.-C. Filliâtre, C. Marché, A. Paskevich.
  
  Formalizing Semantics with an Automatic Program Verifier, in: 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Vienna, Austria, D. Giannakopoulou, D. Kroening (editors), Lecture Notes in Computer Science, Springer, July 2014, vol. 8471, pp. 37–51.
  
  http://hal.inria.fr/hal-01067197
• 64M. Clochard, C. Marché, A. Paskevich.
  
  Verified Programs with Binders, in: Programming Languages meets Program Verification (PLPV), ACM Press, 2014.
  
  http://hal.inria.fr/hal-00913431
• 65S. Conchon.
  
  SMT Techniques and their Applications: from Alt-Ergo to Cubicle, Université Paris-Sud, December 2012, In English, http://www.lri.fr/~conchon/publis/conchonHDR.pdf , Thèse d'habilitation.
• 66S. Conchon, É. Contejean, M. Iguernelala.
  
  Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, in: Tools and Algorithms for the Construction and Analysis of Systems, Saarbrücken, Germany, P. A. Abdulla, K. R. M. Leino (editors), Lecture Notes in Computer Science, Springer, April 2011, vol. 6605, pp. 45-59.
  
  http://hal.inria.fr/hal-00777663
• 67S. Conchon, É. Contejean, M. Iguernelala.
  
  Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation, in: Logical Methods in Computer Science, September 2012, vol. 8, n^o 3, pp. 1–29.
  
  hal.inria.fr/hal-00798082
• 68S. Conchon, D. Declerck, L. Maranget, A. Mebsout.
  
  Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières, in: Vingt-cinquièmes Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014.
  
  https://hal.inria.fr/hal-01088655
• 69S. Conchon, A. Goel, S. Krstić, A. Mebsout, F. Zaïdi.
  
  Invariants for Finite Instances and Beyond, in: FMCAD, Portland, Oregon, États-Unis, October 2013, pp. 61–68.
  
  http://hal.archives-ouvertes.fr/hal-00924640
• 70S. Conchon, M. Iguernelala.
  
  Tuning the Alt-Ergo SMT Solver for B Proof Obligations, in: Abstract State Machines, Alloy, B, VDM, and Z (ABZ), Toulouse, France, Lecture Notes in Computer Science, Springer, June 2014, vol. 8477, pp. 294–297.
  
  https://hal.inria.fr/hal-01093000
• 71S. Conchon, M. Iguernelala, A. Mebsout.
  
  A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo, 2013.
  
  https://hal.archives-ouvertes.fr/hal-00924646
• 72S. Conchon, A. Mebsout, F. Zaïdi.
  
  Vérification de systèmes paramétrés avec Cubicle, in: Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013.
  
  http://hal.inria.fr/hal-00778832
• 73S. Conchon, G. Melquiond, C. Roux, M. Iguernelala.
  
  Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers, in: SMT workshop, Manchester, UK, P. Fontaine, A. Goel (editors), LORIA, 2012, pp. 12–21.
• 74É. Contejean.
  
  Facettes de la preuve, Jeux de reflets entre démonstration automatique et preuve assisté, Université Paris-Sud, June 2014, https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf , Thèse d'habilitation.
  
  https://hal.inria.fr/tel-01089490
• 75M. Dahlweid, M. Moskal, T. Santen, S. Tobies, W. Schulte.
  
  VCC: Contract-based modular verification of concurrent C, in: 31st International Conference on Software Engineering, ICSE 2009, May 16-24, 2009, Vancouver, Canada, Companion Volume, IEEE Comp. Soc. Press, 2009, pp. 429-430.
• 76D. Delahaye, C. Dubois, C. Marché, D. Mentré.
  
  The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations, in: Abstract State Machines, Alloy, B, VDM, and Z (ABZ), Toulouse, France, Lecture Notes in Computer Science, Springer, June 2014, vol. 8477, pp. 290–293.
  
  http://hal.inria.fr/hal-00998092/en/
• 77D. Delahaye, C. Marché, D. Mentré.
  
  Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B, in: Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Paris, France, EasyChair, June 2014.
  
  http://hal.inria.fr/hal-00998094/en/
• 78C. Dross, S. Conchon, J. Kanig, A. Paskevich.
  
  Reasoning with Triggers, in: SMT workshop, Manchester, UK, P. Fontaine, A. Goel (editors), LORIA, 2012.
• 79C. Dross.
  
  Generic Decision Procedures for Axiomatic First-Order Theories, Université Paris-Sud, April 2014.
  
  http://tel.archives-ouvertes.fr/tel-01002190
• 80J.-C. Filliâtre.
  
  Combining Interactive and Automated Theorem Proving in Why3 (invited talk), in: Automation in Proof Assistants 2012, Tallinn, Estonia, K. Heljanko, H. Herbelin (editors), April 2012.
• 81J.-C. Filliâtre.
  
  Combining Interactive and Automated Theorem Proving using Why3 (invited tutorial), in: Second International Workshop on Intermediate Verification Languages (BOOGIE 2012), Berkeley, California, USA, Z. Rakamarić (editor), July 2012.
• 82J.-C. Filliâtre.
  
  Verifying Two Lines of C with Why3: an Exercise in Program Verification, in: Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE), Philadelphia, USA, R. Joshi, P. Müller, A. Podelski (editors), Lecture Notes in Computer Science, Springer, January 2012, vol. 7152, pp. 83–97.
• 83J.-C. Filliâtre.
  
  Deductive Program Verification, in: Programming Languages Mentoring Workshop (PLMW 2013), Rome, Italy, N. Foster, P. Gardner, A. Schmitt, G. Smith, P. Thieman, T. Wrigstad (editors), January 2013.
  
  http://hal.inria.fr/hal-00799190
• 84J.-C. Filliâtre.
  
  One Logic To Use Them All, in: 24th International Conference on Automated Deduction (CADE-24), Lake Placid, USA, Lecture Notes in Artificial Intelligence, Springer, June 2013, vol. 7898, pp. 1–20.
  
  http://hal.inria.fr/hal-00809651/en/
• 85J.-C. Filliâtre, A. Paskevich.
  
  Why3 — Where Programs Meet Provers, in: Proceedings of the 22nd European Symposium on Programming, M. Felleisen, P. Gardner (editors), Lecture Notes in Computer Science, Springer, March 2013, vol. 7792, pp. 125–128.
  
  http://hal.inria.fr/hal-00789533
• 86J.-C. Filliâtre, A. Paskevich, A. Stump.
  
  The 2nd Verified Software Competition: Experience Report, in: COMPARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, Manchester, UK, V. Klebanov, S. Grebing (editors), EasyChair, June 2012.
  
  http://hal.inria.fr/hal-00798777
• 87P. Herms.
  
  Certification of a Tool Chain for Deductive Program Verification, Université Paris-Sud, January 2013.
  
  http://tel.archives-ouvertes.fr/tel-00789543
• 88P. Herms, C. Marché, B. Monate.
  
  A Certified Multi-prover Verification Condition Generator, in: Verified Software: Theories, Tools, Experiments (4th International Conference VSTTE), Philadelphia, USA, R. Joshi, P. Müller, A. Podelski (editors), Lecture Notes in Computer Science, Springer, January 2012, vol. 7152, pp. 2–17.
  
  http://hal.inria.fr/hal-00639977
• 89M. Iguernelala.
  
  Strengthening the Heart of an SMT-Solver: Design and Implementation of Efficient Decision Procedures, Université Paris-Sud, June 2013.
  
  http://tel.archives-ouvertes.fr/tel-00842555
• 90D. Ishii, G. Melquiond, S. Nakajima.
  
  Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus, in: Proceedings of the 10th Conference on Integrated Formal Methods, Turku, Finland, E. B. Johnsen, L. Petre (editors), Lecture Notes in Computer Science, 2013, vol. 7940, pp. 139–153.
  
  http://hal.inria.fr/hal-00806701
• 91J. Kanig, E. Schonberg, C. Dross.
  
  Hi-Lite: the convergence of compiler technology and program verification, in: Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT '12, Boston, USA, B. Brosgol, J. Boleng, S. T. Taft (editors), ACM Press, 2012, pp. 27–34.
• 92G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood.
  
  seL4: Formal verification of an OS kernel, in: Communications of the ACM, June 2010, vol. 53, n^o 6, pp. 107–115.
• 93C. Lelay.
  
  A New Formalization of Power Series in Coq, in: 5th Coq Workshop, Rennes, France, July 2013, pp. 1–2.
  
  http://hal.inria.fr/hal-00880212
• 94C. Lelay.
  
  Coq passe le bac, in: JFLA - Journées francophones des langages applicatifs, Fréjus, France, January 2014.
• 95C. Lelay, G. Melquiond.
  
  Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert, in: Vingt-troisièmes Journées Francophones des Langages Applicatifs, Carnac, France, February 2012.
  
  http://hal.inria.fr/hal-00642206/fr/
• 96X. Leroy.
  
  A formally verified compiler back-end, in: Journal of Automated Reasoning, 2009, vol. 43, n^o 4, pp. 363–446.
  
  http://hal.inria.fr/inria-00360768/en/
• 97C. Marché, A. Tafat.
  
  Weakest Precondition Calculus, revisited using Why3, Inria, December 2012, n^o RR-8185.
  
  http://hal.inria.fr/hal-00766171
• 98C. Marché, A. Tafat.
  
  Calcul de plus faible précondition, revisité en Why3, in: Vingt-quatrièmes Journées Francophones des Langages Applicatifs, Aussois, France, February 2013.
  
  http://hal.inria.fr/hal-00778791
• 99C. Marché.
  
  Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study, in: Science of Computer Programming, March 2014, vol. 96, n^o 3, pp. 279–296.
  
  http://hal.inria.fr/hal-00967124/en
• 100É. Martin-Dorel, G. Melquiond, J.-M. Muller.
  
  Some Issues related to Double Roundings, in: BIT Numerical Mathematics, 2013, vol. 53, n^o 4, pp. 897–924.
  
  http://hal-ens-lyon.archives-ouvertes.fr/ensl-00644408
• 101A. Mebsout.
  
  Invariants inference for model checking of parameterized systems, Université Paris-Sud, September 2014.
  
  https://tel.archives-ouvertes.fr/tel-01073980
• 102G. Melquiond.
  
  Floating-point arithmetic in the Coq system, in: Information and Computation, 2012, vol. 216, pp. 14–23.
  
  http://hal.inria.fr/hal-00797913
• 103G. Melquiond, W. G. Nowak, P. Zimmermann.
  
  Numerical Approximation of the Masser-Gramain Constant to Four Decimal Digits: delta=1.819..., in: Mathematics of Computation, 2013, vol. 82, pp. 1235–1246.
  
  http://hal.inria.fr/hal-00644166/en/
• 104D. Mentré, C. Marché, J.-C. Filliâtre, M. Asuka.
  
  Discharging Proof Obligations from Atelier B using Multiple Automated Provers, in: ABZ'2012 - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Pisa, Italy, S. Reeves, E. Riccobene (editors), Lecture Notes in Computer Science, Springer, June 2012, vol. 7316, pp. 238–251.
  
  http://hal.inria.fr/hal-00681781/en/
• 105J.-M. Muller, N. Brisebarre, F. de Dinechin, C.-P. Jeannerod, V. Lefèvre, G. Melquiond, N. Revol, D. Stehlé, S. Torres.
  
  Handbook of Floating-Point Arithmetic, Birkhäuser, 2010.
• 106P. Neron, A. Tolmach, E. Visser, G. Wachsmuth.
  
  A Theory of Name Resolution, in: ESOP, London, J. Vitek (editor), Lecture Notes in Computer Science, Springer, April 2015, vol. 9032, pp. 205–231.
• 107T. M. T. Nguyen, C. Marché.
  
  Hardware-Dependent Proofs of Numerical Programs, in: Certified Programs and Proofs, J.-P. Jouannaud, Z. Shao (editors), Lecture Notes in Computer Science, Springer, December 2011, pp. 314–329.
  
  http://hal.inria.fr/hal-00772508
• 108T. M. T. Nguyen.
  
  Taking architecture and compiler into account in formal proofs of numerical programs, Université Paris-Sud, June 2012.
  
  http://tel.archives-ouvertes.fr/tel-00710193
• 109M. Norrish.
  
  C Formalised in HOL, University of Cambridge, November 1998.
• 110M. Pereira, J.-C. Filliâtre, S. M. de Sousa.
  
  ARMY: a Deductive Verification Platform for ARM Programs Using Why3, in: INForum 2012, September 2012.
• 111N. Schirmer.
  
  Verification of Sequential Imperative Programs in Isabelle/HOL, Technische Universität München, 2006.
• 112A. Tafat.
  
  Preuves par raffinement de programmes avec pointeurs, Université Paris-Sud, September 2013.
  
  http://tel.archives-ouvertes.fr/tel-00874679
• 113F. de Dinechin, C. Lauter, G. Melquiond.
  
  Certifying the floating-point implementation of an elementary function using Gappa, in: IEEE Transactions on Computers, 2011, vol. 60, n^o 2, pp. 242–253.
  
  http://hal.inria.fr/inria-00533968/en/
• 114L. de Moura, N. Bjørner.
  
  Z3, An Efficient SMT Solver, in: TACAS, Lecture Notes in Computer Science, Springer, 2008, vol. 4963, pp. 337–340.