Tue 14 Jun 2016 14:40 - 15:00 at San Miguel East - Session III Chair(s): Eric Bodden

It is vital to optimize floating-point arithmetic because it is ubiqui- tous, costly, and used in compute-heavy workloads. Implementing precise optimizations correctly, however, is difficult, since devel- opers must account for all the esoteric properties of floating-point arithmetic to ensure that their transformations do not alter the out- put of a program. Manual reasoning is error prone and stifles incor- poration of new optimizations. In this paper, we present an approach to automate reasoning about floating-point optimizations using satisfiability modulo the- ories (SMT) solvers. We implement the approach in LifeJacket, a system for automatically verifying precise floating-point optimiza- tions for the LLVM assembly language. We have used LifeJacket to verify 43 correct optimizations and to discover eight incorrect ones, including three previously unreported problems. LifeJacket is an open source extension of the Alive system for optimization verification

Tue 14 Jun
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

13:30 - 15:00: SOAP - Session III at San Miguel East
Chair(s): Eric BoddenHeinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
SOAP-2016-papers13:30 - 14:20
Matt NoonanGrammaTech, Inc
SOAP-2016-papers14:20 - 14:40
Yan Wang, Hailong ZhangOhio State University, USA, Atanas RountevOhio State University
SOAP-2016-papers14:40 - 15:00
andres NotzliStanford University, Fraser BrownStanford University