Summing Symbols in Mutual Recurrences. - Berkeley R. Churchill; Edmund A. Lamagna (COCOON, 2011)

An Efficient Algorithm for Deriving Summation Identities from Mutual Recurrences. - Berkeley R. Churchill; Edmund A. Lamagna (Discret. Math. Algorithms Appl., 2012)

Data-driven equivalence checking. - Rahul Sharma 001; Eric Schkufza; Berkeley R. Churchill; Alex Aiken (OOPSLA, 2013)

Widening for Control-Flow. - Ben Hardekopf; Ben Wiedermann; Berkeley R. Churchill; Vineeth Kashyap (VMCAI, 2014)

Conditionally correct superoptimization. - Rahul Sharma 001; Eric Schkufza; Berkeley R. Churchill; Alex Aiken (OOPSLA, 2015)

Sound Loop Superoptimization for Google Native Client. - Berkeley R. Churchill; Rahul Sharma 001; J. F. Bastien; Alex Aiken (ASPLOS, 2017)

Semantic program alignment for equivalence checking. - Berkeley R. Churchill; Oded Padon; Rahul Sharma 001; Alex Aiken (PLDI, 2019)

Blackbox equivalence checking of program optimizations. - Berkeley R. Churchill (2019)