@inproceedings{lee2018on,
author = {Lee, Wonyeol and Sharma, Rahul and Aiken, Alex},
title = {On Automatically Proving the Correctness of math.h Implementations},
booktitle = {Principles of Programming Languages 2018 (POPL 2018)},
year = {2018},
month = {January},
abstract = {Industry standard implementations of 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.},
publisher = {ACM},
url = {http://approjects.co.za/?big=en-us/research/publication/automatically-proving-correctness-math-h-implementations/},
pages = {47:01:00-32},
edition = {Principles of Programming Languages 2018 (POPL 2018)},
}