Multi-prover verication of oating-point programs, Fifth IJCAR, LNAI, 2010. ,
Weakest-precondition of unstructured programs, 6th PASTE, 2005. ,
The Spec# Programming System: An Overview, CASSIS'04, p.4969, 2004. ,
DOI : 10.1007/978-3-540-30569-9_3
Proof Obligations Preserving Compilation, FAST'05, p.112126, 2005. ,
DOI : 10.1007/11679219_9
Formal Verication of Floating-Point Programs, 18th ARITH, p.187194, 2007. ,
Hardware-independent proofs of numerical programs, 2nd NASA Formal Methods Symposium, p.1423, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00534410
Proofs of numerical programs when the compiler optimizes, Innovations in Systems and Software Engineering, p.151160, 2011. ,
DOI : 10.1007/s11334-011-0151-6
URL : https://hal.archives-ouvertes.fr/hal-00777639
Automated correctness proofs of machine code programs for a commercial microprocessor, CADE, p.416430, 1992. ,
DOI : 10.1007/3-540-55602-8_181
An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer, vol.box, issue.3, 2003. ,
DOI : 10.1007/s10009-004-0167-4
Java bytecode specication and verication, ACM symposium on Applied computing, 2006. ,
Specication of the IEEE-854 oating-point standard in HOL and PVS, HOL'95, 1995. ,
A certifying compiler for Java, ACM Conference PLDI, 2000. ,
The ASTRE?? Analyzer, ESOP, number 3444 in LNCS, p.2130, 2005. ,
DOI : 10.1007/978-3-540-31987-0_3
Value Plugin Documentation, Carbon version. CEA-List, 2011. ,
Z3, an ecient SMT solver ,
Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software, FMICS, p.5369, 2009. ,
DOI : 10.1007/978-3-642-04570-7_6
Conict detection and resolution for 1, 7th AIAA Aviation, Technology, Integration, and Operations Conference, 2007. ,
Formal Verication of MIX Programs, 2007. ,
The Why/Krakatoa/Caduceus platform for deductive program verication, CAV, p.173177, 2007. ,
Formal verication of oating point trigonometric functions, 3rd FMCAD, p.217233, 2000. ,
Not a number of oating point problems, Journal of Object Technology, vol.5, issue.2, p.7583, 2006. ,
Proving Bounds on Real-Valued Functions with Computations, 4th IJCAR, p.217, 2008. ,
DOI : 10.1007/978-3-540-71070-7_2
URL : https://hal.archives-ouvertes.fr/hal-00180138
The pitfalls of verifying oating-point computations, Transactions on Programming Languages and Systems, vol.30, issue.3, p.12, 2008. ,
Jessie Plugin Tutorial, Beryllium version. INRIA, 2009. ,
Formal verication of machine-code programs, 2008. ,
Proving oating-point numerical programs by analysis of their assembly code, Research Report, vol.7655, 2011. ,
A mechanically checked proof of IEEE compliance of the oating point multiplication, division and square root algorithms of the AMD-K7 processor, LMS Journal of Computation and Mathematics, vol.1, p.148200, 1998. ,