Floating-point verification

被引：0
|
作者：
Harrison, John [1 ]
机构：
[1] Intel Corp, Hillsboro, OR 97124 USA
来源：
JOURNAL OF UNIVERSAL COMPUTER SCIENCE | 2007年 / 13卷 / 05期
关键词：
formal methods; hardware verification;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper overviews the application of formal verification techniques to hardware in general, and to floating-point hardware in particular. A specific challenge is to connect the usual mathematical view of continuous arithmetic operations with the discrete world, in a credible and verifiable way.
引用
收藏
页码：629 / 638
页数：10
相关论文
共 50 条
  • [1] Floating-point verification
    Harrison, J
    [J]. FM 2005: FORMAL METHODS, PROCEEDINGS, 2005, 3582 : 529 - 532
  • [2] Verification of floating-point adders
    Chen, YA
    Bryant, RE
    [J]. COMPUTER AIDED VERIFICATION, 1998, 1427 : 488 - 499
  • [3] Formal Verification of Floating-Point Division
    Kapoor, Ashish
    Ferguson, Warren
    Jain, Himanshu
    Kundu, Sudipta
    [J]. 2023 IEEE 30TH SYMPOSIUM ON COMPUTER ARITHMETIC, ARITH 2023, 2023, : 93 - 96
  • [4] Formal verification of floating-point programs
    Boldo, Sylvie
    Filliatre, Jean-Christophe
    [J]. 18TH IEEE SYMPOSIUM ON COMPUTER ARITHMETIC, PROCEEDINGS, 2007, : 187 - +
  • [5] Automating the Verification of Floating-Point Programs
    Fumex, Clement
    Marche, Claude
    Moy, Yannick
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS (VSTTE 2017), 2017, 10712 : 102 - 119
  • [6] Floating-point verification using theorem proving
    Harrison, John
    [J]. FORMAL METHODS FOR HARDWARE VERIFICATION, 2006, 3965 : 211 - 242
  • [7] Simulation-Based Verification of Floating-Point Division
    Guralnik, Elena
    Aharoni, Merav
    Birnbaum, Ariel J.
    Koyfman, Anatoly
    [J]. IEEE TRANSACTIONS ON COMPUTERS, 2011, 60 (02) : 176 - 188
  • [8] Polynomial function intervals for floating-point software verification
    Duracz, Jan
    Konecny, Michal
    [J]. ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2014, 70 (04) : 351 - 398
  • [9] Verification of the Decimal Floating-Point Square Root Operation
    Ahmed, Amr Sayed
    Fahmy, Hossam
    Kuehne, Ulrich
    [J]. 2014 19TH IEEE EUROPEAN TEST SYMPOSIUM (ETS 2014), 2014,
  • [10] Formal verification of the Pentium®4 floating-point multiplier
    Kaivola, R
    Narasimhan, N
    [J]. DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, 2002 PROCEEDINGS, 2002, : 20 - 27
12345