Research Interests

• Automation for interactive theorem proving
  • Semantic propositional simplification. This uses BDDs, CNF simplification methods, and SAT solvers to simplify instantiations of pure propositional terms. The prototype implementation outperforms existing rewriting based simplifiers, achieving smaller terms without sacrificing speed or fully-expansive proof [11].
  • Propositional decision procedure for interactive proof (with Tjark Weber). This is a fully-expansive integration of SAT solvers with interactive theorem provers, for tautology checking. Achieves multiple orders of magnitude speedup over existing propositional tautology checkers [13]. This is available as part of the HOL4 proof assistant (see tautLib and HolSatLib).
  • Propositional proof compression. This is related to the SAT solver integration. The idea is to remove redudant inferences and thus speed up full-expansive proof reconstruction. The first method constructs a graph-like structure inspired from proof nets, to detect redundancy in ground resolution proofs [9]. It works, but the semantic approach it uses does not scale very well. The second method uses purely syntactic data compression techniques based on suffix trees[10]. It achieves less speedup (about 30-50%) but scales very well.
  • Shallow lazy proofs. This technology allows postponement of fully-expansive proof until it is needed. Unlike previous attempts, it is a purely conservative extension. Handy for working with fast external oracles [7].
  • BDD-based model checking embedded in the HOL theorem prover, interfaced to a high-performance BDD engine for efficiency. It currently has the following features:
    • All steps of the algorithm are proved in HOL, with BDD operations considered atomic [4].
    • Results are returned as theorems that seamlessly incorporate into HOL [4].
    • Model checking for the modal mu-calculus and CTL temporal logics is supported [4,2].
    • Counterexamples and witnesses are generated when appropriate.
    • A fully-automatic counterexample-guided abstraction refinement framework is included. [3]
    Related research papers can be found in Papers. This is now available as part of the HOL4 proof assistant, with documentation.
• Proofs of concurrent programs
  • A framework for automatic Rely-Guarantee proofs (with Richard Bornat). This combines a strongest post-conditions calculus with an automatic stability analysis engine to provide automatic proofs for concurrent threads of a simple guarded command language. The stability analysis uses a combination of model checking, abstract interpretation, and SMT. [12]
  • Manual proofs of non-blocking algorithms (with Richard Bornat). We have constructed a sequence of increasingly cleaner functional correctness proofs for variants of Simpson's 4-slot algorithm, first by naively using a combination of Rely-Guarantee and separation logic, then by refinement. We expect that the techniques developed therein will apply more generally.