[Haskell] PhD position available on `The Productive Use of Failure in Formal Methods'

[Gudmund Grov]

--- apologies for multiple postings ---

The mathematical reasoning research group in the School of Informatics at the University of Edinburgh 
is advertising for a PhD funded by the EPSRC project "AI4FM: Using AI to aid automation of proof search 
in Formal Methods". The proposed topic of the PhD is "The Productive Use of Failure in Formal Methods".

** DESCRIPTION

The task allocated to this PhD will be to analyse ways in which proof attempts fail and are subsequently repaired.
This analysis will be realised in a generic, strategy language for describing and classifying common forms of failure
and repair. The strategy language will, in turn, be used, firstly, to describe how experts recover from failure and, 
secondly, to guide recovery during automated proof search of related proofs. Example failed proofs will be harvested 
from (a) the data from the toolset of Rodin formal methods system, (b) the manual, expert proof attempts on source 
theorems and (c) failed applications to target theorems of proof strategies abstracted from manual expert proofs of
source theorems. Examples of repaired proof attempts will be harvested from the expert's work on failures of both 
types (b) and (c). This work will enhance the abilities of our prototype so it can benefit from initially failed proof 
attempts as well as successful ones.

** DEGREE OF DIFFICULTY 

A challenging project that requires mathematical sophistication, analytic skills and creativity in constructing the strategy language.

** BACKGROUND NEEDED

A background in mathematics, logic or formal methods is required to provide the necessary mathematical maturity to undertake this project.

** CONTACT

If you have any queries, please contact:
- Gudmund Grov: ggrov at inf.ed.ac.uk , or
- Alan Bundy: bundy at inf.ed.ac.uk.

Please use our Schools PhD application page (see below) for applications.

** SOME LINKS

- A description of the proposed PhD project: 
http://wcms.inf.ed.ac.uk/pgrguide/prospectus/projects-container/the-productive-use-of-failure-in-formal-methods
- The web page for the AI4FM project: 
http://www.ai4fm.org/
- Our School's PhD application page: 
http://www.inf.ed.ac.uk/postgraduate/phd.html

** IMPORTANT DATES

There is no deadline for this application, but we do recommended candidates to apply as soon as possible since the position may
be allocated without further notice.

We are fairly flexible on the starting date, but would ideally like it to start between October 2010 and April 2011.

** ABOUT THE RESEARCH INSTITUTION AND RESEARCH GROUP

The Edinburgh School of Informatics obtained the highest volume of 4* activity in its unit of assessment in
RAE 2008. It contains world-class research groups in the areas of theoretical computer science, artificial
intelligence and cognitive science.

The Mathematical Reasoning Group in the School of Informatics has been engaged on the computational
analysis, development and application of mathematical reasoning processes and their interactions since the
mid 1970s (http://dream.inf.ed.ac.uk/). Its work is characterised by its unique blend of computational theory
with artificial intelligence. It has pioneered work on proof planning, tactic learning, and ontology construction
and evolution.


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.