5 papers
Small Proofs from Congruence Closure
Oliver Flatt, Samuel Coward, Max Willsey +2
Satisfiability Modulo Theory (SMT) solvers and equality saturation engines must generate proof certificates from e-graph-based congruence closure procedures to enable verification…
An Interval Arithmetic for Robust Error Estimation
Oliver Flatt, Pavel Panchekha
Interval arithmetic is a simple way to compute a mathematical expression to an arbitrary accuracy, widely used for verifying floating-point computations. Yet this simplicity belies…
Faster Math Functions, Soundly
Ian Briggs, Pavel Panchekha
Standard library implementations of functions like sin and exp optimize for accuracy, not speed, because they are intended for general-purpose use. But applications tolerate inaccu…
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang +3
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a mor…
Combining Tools for Optimization and Analysis of Floating-Point Computations
Heiko Becker, Pavel Pancheckha, Eva Darulova +1
Recent renewed interest in optimizing and analyzing floating-point programs has lead to a diverse array of new tools for numerical programs. These tools are often complementary, ea…