Research
Table of Contents
Objective
My mid-term research objective is to achieve advanced proof automation by leveraging techniques from various fields and applying this automation to build trustworthy systems. I pursue this goal for both theoretical and practical reasons.
On the theoretical side, theorem proving enables machines to fully capture the definitions of mathematical objects provided by users. This sharply contrasts with conventional machine learning techniques, which rely on inductive reasoning, leaving a degree of uncertainty in their conclusions. In theorem proving, however, the conclusions of mechanically proven theorems are 100% certain.
On the practical side, theorem proving is becoming the standard for reliable systems programming. Researchers use theorem provers to define specifications and prove that their implementations meet these specifications. Notable examples include the verification of the seL4 micro-kernel and the CompCert C-compiler. Theorem provers also play a pivotal role in formal scientific advancements, such as the mechanical proofs of famous mathematical conjectures like the Four Colour Theorem and the Kepler Conjecture.
In the long run, I envision large-scale automation of scientific development through automated reasoning. This is why I focus on expressive logics like higher-order logic, rather than less expressive ones: I believe expressive logics are the language of science, and my goal is to achieve robust automated reasoning within this framework. This would enable the automation of scientific development on a broad scale, extending beyond the specific domain of system verification in computer science.
System-Agnostic Approach for Proof Automation
I have predominantly used Isabelle/HOL in my projects to leverage its existing toolsets, including powerful proof tactics and counterexample finders. However, the concepts I develop are generally system-agnostic. In other words, I design techniques that are broad enough to be applied to most, if not all, modern theorem provers for expressive logics that incorporate proof tactics. I then implement these ideas within a specific prover, namely Isabelle/HOL. Consequently, I believe these techniques can be adapted for use with other tactic-based provers, such as The Coq (Rocq) Prover, Lean, and HOL (also known as HOL4), although some modifications may be required to address prover-specific nuances.
Projects
Project List
Here is a list of projects I am currently working on or have worked on. The acronyms correspond to the names used in the project dependency graph below.
- Abduction: Proof By Abduction in Isabelle/HOL
- TemplateBased: Template-Based Conjecturing for Automated Induction in Isabelle/HOL
- GeneticSyn: Genetic Algorithm for Program Synthesis
- SeLFiE: Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- SmarterInduct: Faster Smarter Induction for Isabelle/HOL
- SmartInduct: Smart Induction for Isabelle/HOL (Tool Paper)
- SimpleDataset: Simple Dataset for Proof Method Recommendation in Isabelle/HOL
- LiFtEr: LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
- TowardsEvo: Towards Evolutionary Theorem Proving for Isabelle/HOL
- PaMpeR: PaMpeR: Proof Method Recommendation System for Isabelle/HOL
- GoalOriented: Goal-Oriented Conjecturing for Isabelle/HOL
- PSL: A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
- VerifyC: A framework for the automatic formal verification of refinement from Cogent to C
- Refinement: Refinement through Restraint: Bringing Down the Cost of Verification
- VeriFile: Cogent: Verifying High-Assurance File System Implementations
Project Dependency
This graph summarizes the dependencies of the projects I worked on. You can view the details of each paper by clicking on the corresponding node.
Research Fields
As mentioned above, I draw on expertise from various fields to achieve stronger proof automation. These fields include machine learning, programming languages, evolutionary computation, search, conjecturing, and abductive reasoning. The images below link to sub-pages that explain my projects, organized by research field (most of which are still under construction).
