**I work on STOKE.**

STOKE is a stochastic superoptimizer; it takes an x86 binary and rewrites it for improved performance.

- Software Reliability and Security
- Programing Language Design
- Software Verification
- Type Systems
- Static Analysis
- Applied Category Theory
- functional programing, dependent types, web applications, dependent types, logic, automated theorem proving, combinatorics, graph theory, etc.

- See the current mini-census of regular, connected edge-transitive graphs. This includes data compiled from two other censuses, along with some graphs I discovered on my own.
- A detailed CV is available upon request.

- Sharma R., Schkufza E.,
**Churchill B.**, Aiken A. "Conditionally Correct Superoptimization". OOPSLA 2015. pdf. - Hardekopf B., Wiedermann B.,
**Churchill B.**, Kashyap V. "Widening for Control-Flow". VMCAI 2014. pdf. - Sharma R., Schkufza E.,
**Churchill B.**, Aiken, A. "Data Driven Equivalence Checking." OOPSLA 2013. pdf. **Churchill, B. R.**, and Lamagna, E. A. "Summing symbols in mutual recurrences." In Computing and Combinatorics, B. Fu and D.-Z. Du, Eds., vol. 6842 of Lecture Notes in Computer Science. Springer Berlin / Heidel- berg, 2011, pp. 531-542. pdf. slides.

The original publication is available from www.springerlink.com.

**Churchill, B. R.**, and Lamagna, E. A. "An Efficient Algorithm for Deriving Summation Identities from Mutual Recurrences". Discrete Mathematics, Algorithms and Applications. 04(02), 2012. pdf.