My research involves Extended ML (EML) , a specification language developed by my supervisor, Don (2 n's, 2 l's) Sannella, Andrzej Tarlecki and, more recently, Stefan Kahrs.
For a list of documents I've generated during my research (that I consider fit for publishing on this page, which is a fairly low standard), you can jump to the bottom of this page.
Essentially, EML facilitates the development of programs in the language ML, by allowing developers to write EML programs that contain ML code intermixed with axioms about that code. Development proceeds by transforming the code containing axioms into code containing executable ML that satisfies those axioms. This is an EXTREMELY broad generalization and you should visit the EML home page for more information.
However, it is true that during development the programmer enounters a myriad of proof obligations -- it must be shown that each change made to the code doesn't violate any of the axioms. This is where my project comes in. Work has been done on the nature of these obligations and even how to automatically determine what many of them are (although not necessarily discharge them, but some progress has been made in that area). What I will attempt to do is link EML with PVS, a theorem prover developed at SRI.
A possible scenario proceeds as follows. A developer starts writing EML, and eventually decides to verify that the work done so far is correct. The appropriate files are processed by the tool, which then automatically generates the appropriate theories in PVS. Strategies are automatically applied to discharge as many of the obligations as possible without user interaction, and the developer is then presented with a comforatable interface and interactively attempts to discharge the remaining obligations.
At least that's the plan. Paul Jackson is one of my other supervisors and one of his areas of expertise is PVS. When things get a bit rough with this aspect of the research I expect that I'll be seeing an aweful lot of him.
Most likely, I will also perform a case study. Using the EML methodolgy and the tools I develop to construct a reasonably large program will demonstrate the feasability (or lack thereof) of the system and provide insight into possible future developments.
Below is a list of the papers and documents that I've generated and I deem worthy of appearing on this page. I'm not sure what my criteria for worthiness are, but whatever.