scholarly journals Deductive Verification of Floating-Point Java Programs in KeY

2021 ◽  
pp. 242-261
Author(s):  
Rosa Abbasi ◽  
Jonas Schiffl ◽  
Eva Darulova ◽  
Mattias Ulbrich ◽  
Wolfgang Ahrendt
Keyword(s):  
Programming Language ◽  
Floating Point ◽  
Deductive Verification ◽  
Java Programming ◽  
Special Values ◽  
Floating Point Arithmetic ◽  
Smt Solvers ◽  
Java Programs ◽  
Transcendental Functions ◽  
Point Arithmetic

AbstractDeductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the presence of the special values infinity and ‘Not a Number’ (NaN). In this paper, we present the first floating-point support in a deductive verification tool for the Java programming language. Our support in the KeY verifier handles arithmetic via floating-point decision procedures inside SMT solvers and transcendental functions via axiomatization. We evaluate this integration on new benchmarks, and show that this approach is powerful enough to prove the absence of floating-point special values—often a prerequisite for further reasoning about numerical computations—as well as certain functional properties for realistic benchmarks.

scholarly journals Performance of an Occam/transputer implementation of interval arithmetic

1993 ◽  
Vol 22 (451) ◽  
Author(s):  
Ole Caprani ◽  
Kaj Madsen
Keyword(s):  
Programming Language ◽  
Interval Arithmetic ◽  
Assembly Language ◽  
Floating Point ◽  
Procedure Call ◽  
Floating Point Arithmetic ◽  
Floating Point Unit ◽  
On Chip ◽  
Point Arithmetic ◽  
Parameter Passing

<p>Rounded interval arithmetic is very easy to implement by means of directed rounding arithmetic operators. Such operators are available in the IEEE floating point arithmetic of the transputer. When a few small pieces of assembly language code are used to access the directed rounding operators, the four basic rounded interval arithmetic operators can easily be expressed in the programming language Occam.</p><p>The performance of this implementation is assessed and it is shown that the time consuming part of the calculation are not the directed rounding floating point operations as one might have expected. Most of the time is spent with transport of operands to and from the on-chip floating point unit and the procedure call/parameter passing overhead. Based on this experience the implementation is improved. This implementation runs with 0.15 MIOPS (Million Interval Operations Per Second) or 0.30 MFLOPS on an example interval calculation proposed by Moore. Furthermore, it is demonstrated that an advanced interval language compiler may provide a performance of 0.30 MIOPS or 0.59 MFLOPS on this example calculation.</p>

scholarly journals A Two-Phase Approach for Conditional Floating-Point Verification

2021 ◽  
pp. 43-63
Author(s):  
Debasmita Lohar ◽  
Clothilde Jeangoudoux ◽  
Joshua Sobel ◽  
Eva Darulova ◽  
Maria Christakis
Keyword(s):  
State Of The Art ◽  
Floating Point ◽  
Two Phase ◽  
Phase Approach ◽  
Special Values ◽  
Floating Point Arithmetic ◽  
Roundoff Errors ◽  
Dynamic Analyses ◽  
Point Arithmetic

AbstractTools that automatically prove the absence or detect the presence of large floating-point roundoff errors or the special values NaN and Infinity greatly help developers to reason about the unintuitive nature of floating-point arithmetic. We show that state-of-the-art tools, however, support or provide non-trivial results only for relatively short programs. We propose a framework for combining different static and dynamic analyses that allows to increase their reach beyond what they can do individually. Furthermore, we show how adaptations of existing dynamic and static techniques effectively trade some soundness guarantees for increased scalability, providing conditional verification of floating-point kernels in realistic programs.

Real Floating-Point Arithmetic—The Heart of a Scientific Programming Language

Pascal-Sc ◽  
1987 ◽  
pp. 42-57
Author(s):  
Gerd Bohlender ◽  
Christian Ullrich ◽  
Jürgen Wolff von Gudenberg ◽  
Louis B. Rall
Keyword(s):  
Programming Language ◽  
Floating Point ◽  
Floating Point Arithmetic ◽  
Point Arithmetic

scholarly journals Numerical algorithms for high-performance computational science

2020 ◽  
Vol 378 (2166) ◽  
pp. 20190066 ◽  
Author(s):  
Jack Dongarra ◽  
Laura Grigori ◽  
Nicholas J. Higham
Keyword(s):  
High Performance ◽  
Numerical Algorithms ◽  
Computational Science ◽  
Floating Point ◽  
Important Criterion ◽  
Data Movement ◽  
Floating Point Arithmetic ◽  
High Performance Computers ◽  
Point Arithmetic ◽  
Speed And Accuracy

A number of features of today’s high-performance computers make it challenging to exploit these machines fully for computational science. These include increasing core counts but stagnant clock frequencies; the high cost of data movement; use of accelerators (GPUs, FPGAs, coprocessors), making architectures increasingly heterogeneous; and multi- ple precisions of floating-point arithmetic, including half-precision. Moreover, as well as maximizing speed and accuracy, minimizing energy consumption is an important criterion. New generations of algorithms are needed to tackle these challenges. We discuss some approaches that we can take to develop numerical algorithms for high-performance computational science, with a view to exploiting the next generation of supercomputers. This article is part of a discussion meeting issue ‘Numerical algorithms for high-performance computational science’.

Fast and robust mesh arrangements using floating-point arithmetic

2020 ◽  
Vol 39 (6) ◽  
pp. 1-16
Author(s):  
Gianmarco Cherchi ◽  
Marco Livesu ◽  
Riccardo Scateni ◽  
Marco Attene
Keyword(s):  
Floating Point ◽  
Floating Point Arithmetic ◽  
Point Arithmetic

Floating-point arithmetic with 84-bit numbers

1964 ◽  
Vol 7 (1) ◽  
pp. 10-13 ◽  
Author(s):  
Robert T. Gregory ◽  
James L. Raney
Keyword(s):  
Floating Point ◽  
Floating Point Arithmetic ◽  
Point Arithmetic
Sign in / Sign up

Export Citation Format

Share Document