8 citations · 21 across the 22 of their papers we have counts for
5 papers · 1 filter
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…
Automatic Generation of Complete Polynomial Interpolation Hardware Design Space
Bryce Orloski, Samuel Coward, Theo Drane
Hardware implementations of complex functions regularly deploy piecewise polynomial approximations. This work determines the complete design space of piecewise polynomial approxima…
Combining E-Graphs with Abstract Interpretation
Samuel Coward, George A. Constantinides, Theo Drane
E-graphs are a data structure that compactly represents equivalent expressions. They are constructed via the repeated application of rewrite rules. Often in practical applications,…
Automatic Datapath Optimization using E-Graphs
Samuel Coward, George A. Constantinides, Theo Drane
Manual optimization of Register Transfer Level (RTL) datapath is commonplace in industry but holds back development as it can be very time consuming. We utilize the fact that a com…
Abstract Interpretation on E-Graphs
Samuel Coward, George A. Constantinides, Theo Drane
Recent e-graph applications have typically considered concrete semantics of expressions, where the notion of equivalence stems from concrete interpretation of expressions. However,…