I will be attending (and talking at!) the Doctoral Symposium at FM2012 (18th International Symposium on Formal Methods) in Paris next week. A preprint of the accepted publication on my PhD research is available from here, as well as a Newcastle technical report.
The publication and talk uses the current working title of my PhD: Inferring the Proof Process. I try to cover the ideas of what I am aiming for with my research (i.e. what describes a proof process? how can we capture and understand the expert’s ideas?), as well as current results (the ProofProcess framework) and future directions (i.e. how can we automate the proof process capture and analysis?)
The actual abstract is below:
This PhD project aims to investigate how enough information can be collected from an interactive formal proof to capture an expert’s ideas as a high-level proof process. It would then serve for extracting proof strategies to facilitate proof automation. Ways of inferring this proof process automatically are explored; and a family of tools is developed to capture the different proof processes and their features.
Early release time!
I got around to creating proper build environments for all the code I have been working on. Using Eclipse Tycho I was able to create Maven build configurations for all the projects. Now producing Eclipse update sites for end-users is (mostly) a single-click process.
So finally I can offer easy install sites for Isabelle/Eclipse and the ProofProcess framework. I have also added an update site for CZT Eclipse plug-ins, which now feature integration with Z/EVES theorem prover.
Note that these are early technical preview releases. This means that we have been using the tools ourselves, but they still have rough edges and are likely to change. Also, the documentation is quite lacking—we hope to improve in all of these areas! So please report any problems/issues/suggestions you encounter.
Isabelle/Eclipse provides an Eclipse-based Prover IDE for Isabelle proof assistant, based on Isabelle/Scala framework. It started as a port of Isabelle/jEdit Prover IDE. To install the latest version, point your Eclipse IDE to this update site:
ProofProcess framework is the tool goal of my PhD. Currently its core is available. It aims to capture, store, analyse and display proof process data from Isabelle and Z/EVES provers in Eclipse-based interface. The current version is available from this update site:
The data capture should start automatically with Isabelle/Eclipse or Z/EVES theorem provers and there are views available to display it. Note that scalability has not been tested much yet.
We have updated Eclipse plug-ins for Community Z Tools and added integration with Z/EVES theorem prover for verifying Z specifications. The functionality will be released as CZT 1.6, but until we get around to doing that, the ‘nightly’ release of the Eclipse plug-ins is available from this update site:
Hopefully these will allow you to get a taste of the tools. Please try them out and check back for updates here and on their respective web sites.
It does not bode well to have a website titled “notes on PhD research” without actually talking about the research. I will try to provide a glimpse into what I have been up to in my PhD—and what I am trying to achieve at the end of it.
My research interests lie in formal methods, software verification, and—especially—theorem proving as part of the formal system development. The state of art in theorem proving of “industrial” (as opposed to mathematical) proofs is that still quite significant effort is spent in interactive proof. In AI4FM project we aim to increase automation here by learning from an expert doing proof and then completing similar proofs automatically.
My PhD research is most concerned with capturing and understanding the interactive proof. I am investigating how to capture expert’s ideas as a high-level proof process. The proof process data with sufficient information could then serve to extract reusable strategies and eventually replay them on similar proofs.
I am developing some of the ideas as a generic ProofProcess framework. It serves as the infrastructure to capture and infer the proof process for different theorem provers. The system links closely with proof assistants such as Isabelle or Z/EVES (via new prover IDEs/tools).
This is my approach to managing references in a single master BibTeX file. By putting the bibliography file in a Git repository and then using it as a submodule of Git repositories for my papers, I get a portable, versioned and centralised solution to reference management. Here is how I do it.
I am still staying away from the social aspect of scientific reference management, à la CiteULike or Mendeley. Instead, I manage my research references the old-fashioned way: as BibTeX files using the excellent BibDesk. So when I set up this website I looked for a WordPress plugin to embed my BibTeX files into a page. I opted for a plugin instead of various bibtex2html options to avoid manually updating the page when BibTeX file changes.
It has been recently updated to version 0.4, which features a couple of my contributions: the plain citation style and av-bibtex entry template. The plain citation style aims to mimic its namesake in LaTeX distributions. The av-bibtex template adds support for displaying
URL fields: it
is used in my publications page. Yes, it is not a perfect showcase with a couple entries, but hey, I am working on adding more during my PhD!