Research Interests

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

Current Projects

  • Smart Testing for Web Applications
    Developers testing web applications in MVC frameworks, like Rails, often employ integration (end-to-end) tests. These require intensive human work to enumerate possible use-cases. A more traditional testing approach is to use a web crawler, for example, to check for dead links. However, crawlers lack the ability to reach much of the state of an application. This project proposes an intermediate approach, where the developer writes test code in a DSL which compiles into a crawler that explores the site. The goal is to make these integration tests more robust and maintainable, while being more systematic in exploring states and checking specifications.



  • 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