Bit-Vector Approximations of Floating-Point Arithmetic

Abstract: The use of floating-point numbers in safety-critical applications shows a need to efficiently and automatically reason about them. One approach is to use Satisfiability modulo theories (SMT). The naive approach to using SMT does not scale well. Previous work suggests approximations as a scalable solution. Zeljic, Backeman, Wintersteiger, and Rümmer have created a framework called UppSAT for iterative approximations. The approximations created with UppSAT use a precision to indicate how approximate the formula is. Floating-point can be approximated by the simpler fixed-point format. This provides the benefit of not having to encode the rounding modes and special values. It also enables efficient encodings of the operations as bit-vectors. Zeljic et al. have implemented such an approximation in UppSAT. The precision of the approximation indicates the amount of bits that the numbers use. This thesis aims to improve the way that the approximation handles precision: by providing two new strategies for increasing it, increasing the detail, and changing the maximum. One of the two new strategies is implemented. Both strategies are based on the idea to calculate the amount of bits needed to represent a float as fixed-point. The implemented strategy performs worse than the current but solves test cases that the current is not able to solve. The reason for the performance is probably a too fast increase of the precision and that the same precision is used for the whole formula. Even though the implemented strategy is worse, the new strategies and precision domain can provide a base to build on when further improving the approximation and also help to show that fixed-point and approximations, in general, are suitable for reasoning about floating-point and that there are more approximations to investigate.