Hardware-Independent Proofs of Numerical ProgramsOn recent architectures, a numerical program may give different answers depending on the execution hardware and the compilation. Our goal is to formally prove properties about numerical programs that are true for multiple architectures and compilers. We propose an approach that states the rounding error of each floating-point computation whatever the environment. This approach is implemented in the Frama-C platform for static analysis of C code. Small case studies using this approach are entirely and automatically proved
Document ID
20100018555
Acquisition Source
Langley Research Center
Document Type
Conference Paper
Authors
Boldo, Sylvie (Institut National de Recherche d'Informatique et d'Automatique France)
Nguyen, Thi Minh Tuyen
Date Acquired
August 24, 2013
Publication Date
April 1, 2010
Publication Information
Publication: Proceedings of the Second NASA Formal Methods Symposium