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

Author(s):  
Rosa Abbasi ◽  
Jonas Schiffl ◽  
Eva Darulova ◽  
Mattias Ulbrich ◽  
Wolfgang Ahrendt
Author(s):  
Rosa Abbasi ◽  
Jonas Schiffl ◽  
Eva Darulova ◽  
Mattias Ulbrich ◽  
Wolfgang Ahrendt

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.


10.29007/wh99 ◽  
2018 ◽  
Author(s):  
Sylvain Conchon ◽  
Guillaume Melquiond ◽  
Cody Roux ◽  
Mohamed Iguernelala

The treatment of the axiomatic theory of floating-point numbers isout of reach of current SMT solvers, especially when it comes toautomatic reasoning on approximation errors. In this paper, wedescribe a dedicated procedure for such a theory, which provides aninterface akin to the instantiation mechanism of an SMT solver.This procedure is based on the approach of the Gappa tool: itperforms saturation of consequences of the axioms, in order torefine bounds on expressions. In addition to the original approach,bounds are further refined by a constraint solver for lineararithmetic. Combined with the natural support for equalitiesprovided by SMT solvers, our approach improves the treatment ofgoals coming from deductive verification of numeric programs. Wehave implemented it in the Alt-Ergo SMT solver.


2020 ◽  
Vol 33 (109) ◽  
pp. 21-31
Author(s):  
І. Ya. Zeleneva ◽  
Т. V. Golub ◽  
T. S. Diachuk ◽  
А. Ye. Didenko

The purpose of these studies is to develop an effective structure and internal functional blocks of a digital computing device – an adder, that performs addition and subtraction operations on floating- point numbers presented in IEEE Std 754TM-2008 format. To improve the characteristics of the adder, the circuit uses conveying, that is, division into levels, each of which performs a specific action on numbers. This allows you to perform addition / subtraction operations on several numbers at the same time, which increas- es the performance of calculations, and also makes the adder suitable for use in modern synchronous cir- cuits. Each block of the conveyor structure of the adder on FPGA is synthesized as a separate project of a digital functional unit, and thus, the overall task is divided into separate subtasks, which facilitates experi- mental testing and phased debugging of the entire device. Experimental studies were performed using EDA Quartus II. The developed circuit was modeled on FPGAs of the Stratix III and Cyclone III family. An ana- logue of the developed circuit was a functionally similar device from Altera. A comparative analysis is made and reasoned conclusions are drawn that the performance improvement is achieved due to the conveyor structure of the adder. Implementation of arithmetic over the floating-point numbers on programmable logic integrated cir- cuits, in particular on FPGA, has such advantages as flexibility of use and low production costs, and also provides the opportunity to solve problems for which there are no ready-made solutions in the form of stand- ard devices presented on the market. The developed adder has a wide scope, since most modern computing devices need to process floating-point numbers. The proposed conveyor model of the adder is quite simple to implement on the FPGA and can be an alternative to using built-in multipliers and processor cores in cases where the complex functionality of these devices is redundant for a specific task.


2012 ◽  
Vol 1 (6) ◽  
pp. 67-68
Author(s):  
M. Somasekhar M. Somasekhar ◽  
Keyword(s):  

Sign in / Sign up

Export Citation Format

Share Document