user

The pitfalls of verifying floating-point computations

被引：92
|
作者：
Monniaux, David [1 ]
机构：
[1] Ecole Normale Super, CNRS, Paris, France
来源：
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 2008年 / 30卷 / 03期
关键词：
languages; verification; abstract interpretation; static analysis; program testing; floating point; embedded software; safety-critical software; x87; IA32; AMD64; PowerPC; FPU; rounding; IEEE-754;
D O I：
10.1145/1353445.1353446
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Current critical systems often use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change according to many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions for implementing in analysis software.
引用
收藏
页数：41
相关论文
共 50 条
  • [1] A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
    Ramananandro, Tahina
    Mountcastle, Paul
    Meister, Benoit
    Lethin, Richard
    [J]. PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16), 2016, : 15 - 26
  • [2] Termination of Floating-Point Computations
    Alexander Serebrenik
    Danny De Schreye
    [J]. Journal of Automated Reasoning, 2005, 34 : 141 - 177
  • [3] Termination of floating-point computations
    Serebrenik, A
    De Schreye, D
    [J]. JOURNAL OF AUTOMATED REASONING, 2005, 34 (02) : 141 - 177
  • [4] Verified Compilation of Floating-Point Computations
    Boldo, Sylvie
    Jourdan, Jacques-Henri
    Leroy, Xavier
    Melquiond, Guillaume
    [J]. JOURNAL OF AUTOMATED REASONING, 2015, 54 (02) : 135 - 163
  • [5] Faithfully Rounded Floating-point Computations
    Lange, Marko
    Rump, Siegfried M.
    [J]. ACM TRANSACTIONS ON MATHEMATICAL SOFTWARE, 2020, 46 (03):
  • [6] Verified Compilation of Floating-Point Computations
    Sylvie Boldo
    Jacques-Henri Jourdan
    Xavier Leroy
    Guillaume Melquiond
    [J]. Journal of Automated Reasoning, 2015, 54 : 135 - 163
  • [7] Symbolic execution of floating-point computations
    Botella, Bernard
    Gotlieb, Arnaud
    Michel, Claude
    [J]. SOFTWARE TESTING VERIFICATION & RELIABILITY, 2006, 16 (02): : 97 - 121
  • [8] Floating-point computations on reconfigurable computers
    Morris, Gerald R.
    [J]. PROCEEDINGS OF THE HPCMP USERS GROUP CONFERENCE 2007, 2007, : 339 - 344
  • [9] Verifying Bit-Manipulations of Floating-Point
    Lee, Wonyeol
    Sharma, Rahul
    Aiken, Alex
    [J]. ACM SIGPLAN NOTICES, 2016, 51 (06) : 70 - 84
  • [10] An Interval Compiler for Sound Floating-Point Computations
    Rivera, Joao
    Franchetti, Franz
    Puschel, Markus
    [J]. CGO '21: PROCEEDINGS OF THE 2021 IEEE/ACM INTERNATIONAL SYMPOSIUM ON CODE GENERATION AND OPTIMIZATION (CGO), 2021, : 52 - 64
12345