PhD studentship available for September/October 2012 start

• Location: Department of Computer Science, University of Leicester 
• Supervisors: Dr Neil Walkinshaw, Prof Rajeev Raman
• Stipend:   £13,590 pa
• Closing Date:  Thursday March 8, 2012
• Interview Date: Mid March 

The PhD studentship, jointly funded by EPSRC and the College of Science and Engineering of the University of Leicester, UK, is available at the Department of Computer Science for September/October 2012 start. The funding covers fees (at home/EU level) and stipend for three years. The amount of the stipend is currently £13,590 per annum. The studentship is intended for a student with home/EU fee status (see the EPSRC rules for student eligibility).

The Department of Computer Science offers a highly collegiate and stimulating environment for research career development. The prospective student will work within an ambitious research team that is internationally recognised and will be expected to contribute to the strong profile of the department through participation in the development and publication of international-quality research results.  

The aim of the project is to boost the effectiveness of theorem provers, which are used extensively for the verification of software and hardware systems. As such, in boosting the ability to verify these devices, they do not merely become safer and more reliable, but also become cheaper to manufacture.

Required and desired qualifications

Applicants should hold a first-class honours degree or equivalent in computer science (or a closely-related discipline), experience in programming and a good command of English. Applicants are not required to have completed an MSc degree, though holding such a degree (or being in the process of obtaining one) would also be an advantage. 

Applicants must possess strong programming skills. A strong background in the formal aspects of Computer Science, and knowledge of data mining would be especially desirable.

The research project to be conducted is outlined below. 

Research Project Description

Title: Boosting Automated Reasoning by Mining Proof Strategies

Automated reasoning systems (or theorem provers) can automate the process of reasoning about complex systems. Given a basic set of rules about the system in question, along with “goal” - a hypothesis about the system, theorem provers can automatically apply the rules to build 'proofs' that either confirm or rule out the hypothesis. Such tools have become increasingly commonplace, especially in the domain of hardware and software verification, where they play an important role in the process of establishing the correctness of designs, particularly for safety-critical systems.  

The problem is that the capabilities of theorem provers are currently restricted. They rely heavily on the expertise of their users. Finding a suitable sequence of `proof-steps’ is very difficult. 

This PhD will devise a solution to this important limitation. There exist large repositories of existing successful proofs. These will include lots of examples of successful proofs, where humans have provided the necessary inputs using their expertise and intuition to elicit a successful proof. The aim will be to devise a novel “tactic mining” strategy that can use these repositories to automatically identify effective tactics that can be more widely applied. This will boost the power of theorem provers, and reduce their reliance on human intervention. 

Informal Enquiries:

Informal enquiries are welcome - please contact Dr. Neil Walkinshaw (nw91 at leicester dot ac dot uk) or Professor Rajeev Raman (r dot raman at leicester dot ac dot uk).

Application process:

To apply, simply follow our three-point checklist:

1. Draft a brief personal statement explaining why you would like to work in this area and describing any relevant research experience (including any research projects that you have undertaken - for example, as part of a previous degree - and listing any academic work you have published or which is currently in press awaiting publication). Your personal statement should be no more than 1,000 words.
2. Prepare your supporting documents 
3. Submit your online application or apply by post

The closing date for applications is 8th March 2012.

IMPORTANT - In the Fees and Financial Support section of the application, you must state that you wish to be considered for this "PhD Studentship (Ref. Neil Walkinshaw)”