Current Project

I work on STOKE.

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

Research Interests

  • 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.




  • 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


  • 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.


  • Churchill, B. R. "Semi-Symmetric Graphs of Vaence 5" (Mathematics Senior Thesis). 2012. pdf. slides