Mon 15 Jun 2026 11:30 - 11:55 at Meadows CD - Session 2

Equality Saturation (EqSat) is a powerful technique for program optimization, systematically exploring the search space of candidate programs to overcome the phase ordering problem.

However, the feasibility and performance of EqSat rely heavily on the specific rewrite rules used to derive equivalent programs. These rule sets are typically handcrafted, requiring extensive domain expertise and carrying the risk of missing valuable transformations.

In this work, we evaluate Knuth-Bendix Completion (KBC) as a method for automatically generating and augmenting rewrite rules for EqSat. Our experiments show faster optimization as well as reaching better terms with previously missed optimizations.

Mon 15 Jun

Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:20
Session 2EGRAPHS at Meadows CD
10:40
25m
Talk
A Semi-Persistent E-Graph with Native AC Canonization and Leapfrog AC Matching.
EGRAPHS
Remi Delmas Amazon Web Services
Pre-print
11:05
25m
Talk
Associativity and Commutativity in Equality Saturation
EGRAPHS
Tarik Rosin Saarland University, Marcel Ullrich Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus
Pre-print
11:30
25m
Talk
Augmenting Rewrite Rule Sets via Knuth-Bendix Completion
EGRAPHS
Michael Schifferer Saarland University, Marcel Ullrich Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus
Pre-print
11:55
25m
Talk
E-graphs modulo theoriesRemote
EGRAPHS
Sofia Brookie Chalmers University of Technology