Fri 12 Jan 2018 11:20 - 11:45 at Bunker Hill - Testing and Verification Chair(s): Santosh Nagarakatte

Industry standard implementations of {\tt math.h} claim (often without formal proof) tight bounds on floating-point errors. We demonstrate a novel static analysis that proves these bounds and verifies the correctness of these implementations. Our key insight is a reduction of this verification task to a set of mathematical optimization problems that can be solved by off-the-shelf computer algebra systems. We use this analysis to prove the correctness of implementations in Intel’s math library automatically. Prior to this work, these implementations could only be verified with significant manual effort.

Fri 12 Jan

10:30 - 12:10: Research Papers - Testing and Verification at Bunker Hill
Chair(s): Santosh NagarakatteRutgers University, USA
POPL-2018-papers10:30 - 10:55
Leonidas LampropoulosUniversity of Pennsylvania, Zoe ParaskevopoulouPrinceton University, Benjamin C. PierceUniversity of Pennsylvania
POPL-2018-papers10:55 - 11:20
POPL-2018-papers11:20 - 11:45
Wonyeol LeeStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford University
POPL-2018-papers11:45 - 12:10
Shelly GrossmanTel Aviv University, Ittai AbrahamVMWare Research, Guy Golan-GuetaVMWare Research, Yan MichalevskyStanford University, Noam RinetzkyTel Aviv University, Mooly SagivTel Aviv University, Yoni ZoharTel Aviv University