Research

  • I have started working as a research associate in Taming Concurrency project, trying to improve reasoning about concurrency in software. More updates on this will be added in due course.
  • I have completed my PhD thesis “Capturing Proof Process” in 2015.

I am interested in using formal methods and theorem proving to develop software systems with that extra level of assurance. Theorem proving allows justifying the formal development, but is a laborious and still quite manual task. In my PhD I am looking how to understand and learn from previous proofs to complete similar ones automatically.

Understanding proof strategies

Formal methods can be used to develop software systems from abstract specification down to concrete code. The specifications and designs can be defined with mathematical rigour and justified by proving associated theorems. This way we can achieve assurance in the developed system. The ideal is to achieve a correct system—one we can trust completely.

In AI4FM we are looking how to assist with the theorem proving part. The amount of interactive proof needed in industrial scale formal development can be quite massive. We are investigating how to learn from one interactive proof so that other similar proofs can be completed automatically. More details on why and how are available in our project website.

In my PhD I am investigating how to understand interactive proof. Let’s say that we have a formal development (e.g. an abstract specification), which is justified by proving associated theorems using interactive proof assistant (such as Isabelle or Event-B/Rodin). An expert comes in and uses the tool to discharge a proof obligation interactively by performing a number of proof steps. I want to capture how he did it—but as a high-level proof process. This leads to a number of questions: how can we collect enough information to do that? What describes the proof process? Can we do that automatically? The goal is to capture the proof process with sufficient information to extract proof strategies that facilitate proof automation.

ProofProcess framework

Currently I am bringing some of the ideas to life by developing a new ProofProcess framework. It provides the infrastructure to describe and capture high-level proof process backed by low-level proof steps. The aim is to create a generic framework, which could be used with different proof assistants. The tools would closely (and ideally invisibly) integrate with proof assistants to capture and infer the proof process.

The framework is developed as a generic core with prover-specific extensions. Currently I have prototype implementations for Isabelle (via Isabelle/Eclipse) and Z/EVES (via CZT-Z/EVES) proof assistants.

Supporting tool development

To support the ProofProcess framework, we have some more developments to add to the tool chain:

  • Isabelle/Eclipse provides Eclipse IDE integration for Isabelle proof assistant. It uses the Isabelle/Scala layer and the PIDE infrastructure as in the official Isabelle/jEdit Prover IDE.

  • CZT-Eclipse and CZT-Z/EVES are parts of the Community Z Tools and provide Eclipse-based solution for developing and verifying formal Z specifications. We have updated the Eclipse editors and provided an integration with Z/EVES theorem prover—they will be available in the upcoming CZT 1.6 release.