The Alt-Ergo automated theorem prover, 2008. ,
SMT techniques and their applications: from Alt-Ergo to Cubicle , Thèse d'habilitation, 2012. ,
CVC3, 19th International Conference on Computer Aided Verification, pp.298-302, 2007. ,
DOI : 10.1007/978-3-540-73368-3_34
Z3: An Efficient SMT Solver, Lecture Notes in Computer Science, vol.4963, pp.337-340, 2008. ,
DOI : 10.1007/978-3-540-78800-3_24
Proving Bounds on Real-Valued Functions with Computations, Proceedings of the 4th International Joint Conference on Automated Reasoning, pp.2-17, 2008. ,
DOI : 10.1007/978-3-540-71070-7_2
URL : https://hal.archives-ouvertes.fr/hal-00180138
Interactive Theorem Proving and Program Development, 2004. ,
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237
ACSL: ANSI/ISO C Specification Language, version 1, 2009. ,
The Jessie plugin for Deduction Verification in Frama-C ? Tutorial and Reference Manual, INRIA & LRI, 2011. ,
Modular inference of subprogram contracts for safety checking, Journal of Symbolic Computation, vol.45, issue.11, pp.1184-1211, 2010. ,
DOI : 10.1016/j.jsc.2010.06.004
URL : https://hal.archives-ouvertes.fr/inria-00534331
An experience report on the verification of algorithms in the C++ standard library using Frama-C, Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, pp.191-204, 2010. ,
Quaternions and Rotation Sequences: A Primer With Applications to Orbits, Aerospace, and Virtual Reality, 1999. ,
DOI : 10.7546/giq-1-2000-127-143
Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs, Mathematics in Computer Science, vol.1, issue.2, pp.377-393, 2011. ,
DOI : 10.1007/s11786-011-0099-9
URL : https://hal.archives-ouvertes.fr/hal-00777605
The 2nd verified software competition: Experience report, COM- PARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012. ,
The 1st Verified Software Competition: Experience Report, FM, pp.154-168, 2011. ,
DOI : 10.1007/978-3-540-71067-7_6
Java2 implementation notes, Tech. rep., http://secure.ucd.ie/products/opensource, 2007. ,
Using First-Order Theorem Provers in the Jahob Data Structure Verification System, 8th International Conference on Verification, Model Checking, and Abstract Interpretation, pp.74-88, 2007. ,
DOI : 10.1007/978-3-540-69738-1_5
An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer, vol.box, issue.3, pp.212-232, 2005. ,
DOI : 10.1007/s10009-004-0167-4
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
The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS'04), pp.49-69, 2004. ,
DOI : 10.1007/978-3-540-30569-9_3
SPARK?an annotated Ada subset for safetycritical programming, Proceedings of the conference on TRI-ADA'90, pp.392-402, 1990. ,
Multi-Prover Verification of Floating-Point Programs, Fifth International Joint Conference on Automated Reasoning, pp.127-141, 2010. ,
DOI : 10.1007/978-3-642-14203-1_11
URL : https://hal.archives-ouvertes.fr/inria-00534333
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
Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013. ,
DOI : 10.1007/978-3-642-37036-6_8
The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems, vol.30, issue.3, 2008. ,
DOI : 10.1145/1353445.1353446
URL : https://hal.archives-ouvertes.fr/hal-00128124
Hardware-independent proofs of numerical programs, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, pp.14-23, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00534410
Proofs of numerical programs when the compiler optimizes, Innovations in Systems and Software Engineering, vol.1, issue.3, pp.151-160, 2011. ,
DOI : 10.1007/s11334-011-0151-6
URL : https://hal.archives-ouvertes.fr/hal-00777639
Hardware-Dependent Proofs of Numerical Programs, Certified Programs and Proofs, pp.314-329, 2011. ,
DOI : 10.1112/S1461157000000176
URL : https://hal.archives-ouvertes.fr/hal-00772508
Taking architecture and compiler into account in formal proofs of numerical programs, Thèse de doctorat, 2012. ,
URL : https://hal.archives-ouvertes.fr/tel-00710193
Floating-point arithmetic in the Coq system, Information and Computation, vol.216, pp.14-23, 2012. ,
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions, Journal of Automated Reasoning, vol.7, issue.4, pp.175-205, 2010. ,
DOI : 10.1007/s10817-009-9149-2
Separation analysis for deductive verification, in: Heap Analysis and Verification (HAV'07), pp.81-93, 2007. ,
Specification of the IEEE-854 floating-point standard in HOL and PVS, HOL95: 8th International Workshop on Higher- Order Logic Theorem Proving and Its Applications, 1995. ,
Abstract, LMS Journal of Computation and Mathematics, vol.11, pp.148-200, 1998. ,
DOI : 10.1112/S1461157000000176
Formal Verification of Floating Point Trigonometric Functions, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, pp.217-233, 2000. ,
DOI : 10.1007/3-540-40922-X_14
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, 14th International Conference on Theorem Proving in Higher Order Logics, pp.169-184, 2001. ,
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285
Floating point verification in HOL light: The exponential function, Formal Methods in System Design, vol.16, issue.3, pp.271-305, 2000. ,
DOI : 10.1007/BFb0000475
Formal Verification of Floating-Point Programs, 18th IEEE Symposium on Computer Arithmetic (ARITH '07), pp.187-194, 2007. ,
DOI : 10.1109/ARITH.2007.20
URL : https://hal.archives-ouvertes.fr/hal-01174892
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.200, issue.25???28, pp.423-456, 2013. ,
DOI : 10.1007/s10817-012-9255-4
URL : https://hal.archives-ouvertes.fr/hal-00649240
Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors, 13th European Symposium on Programming (ESOP), pp.3-17, 2004. ,
DOI : 10.1007/978-3-540-24725-8_2
Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software, FMICS LNCS, vol.5825, pp.53-69, 2009. ,
DOI : 10.1007/978-3-642-04570-7_6
Verification of Numerical Programs: From Real Numbers to Floating Point Numbers, NASA Formal Methods, 5th International Symposium, pp.441-446, 2013. ,
DOI : 10.1007/978-3-642-38088-4_31
Conflict detection and resolution for 1, Proceedings of the 7th AIAA Aviation, Technology, Integration, and Operations Conference, pp.2007-7737, 2007. ,
Mechanized Semantics for the Clight Subset of the C Language, Journal of Automated Reasoning, vol.29, issue.6, pp.263-288, 2009. ,
DOI : 10.1007/s10817-009-9148-3
URL : https://hal.archives-ouvertes.fr/inria-00352524
Certification of a tool chain for deductive program verification, Thèse de doctorat, 2013. ,
URL : https://hal.archives-ouvertes.fr/tel-00789543