Usage of Static Analysis for Model Checking Liveness Properties of Heap Manipulating Programs

The Department of Computer Science is pleased to offer this full-time PhD studentship available for immediate start. The studentship - supported under the Microsoft Research Fellowships - will pay full-time University UK/EU tuition fees for three years and include an annual tax-free stipend of £13,590.

Research Areas and Supervision

One of the major challenges facing the successful application of model checking in software is the ability to analyze programs that use dynamic memory allocation and sophisticated data structures.

This project aims to investigate the advantages of considering more expressive versions of Kripke structures (such as modal transition systems and disjunctive modal transition systems) as an abstraction domain for shape analysis.

The project has two facets:

• In the context of static analysis, study the principles for extending the functionality of static analysis tools (such as TVLA) with this ability and the implications regarding preservation of branching-time temporal-logic properties and their automatic extraction.
• In the context of model checking, study the additional opportunities that are afforded by the augmentation of abstract heap information with fairness information in order to enable model checking of general temporal logic specifications that rely on boundedness and finiteness of heaps.

Further information about the research project >

The successful applicant will be supervised by Dr Nir Piterman (University of Leicester) and Dr Josh Berdine (Microsoft Research).

Additional Information

Students under this scheme are often chosen for a three month internship at Microsoft Research. During the internship students work with Microsoft researchers on Microsoft projects. Interns at Microsoft are paid separately according to Microsoft standards. There is no guarantee that the successful applicant will be chosen for an internship.

The successful applicant will receive from Microsoft Research a laptop for use over the duration of the studentship; this laptop will be awarded to the student upon successful completion of the PhD.

Entry Requirements

Applicants must have a first-class honours degree (or equivalent qualification) in computer science or mathematics and meet the University's standard English language entry requirements. Applicants should have experience in programming and an aptitude for mathematical subjects. Knowledge of formal methods, logic, static analysis, or model checking would be an advantage and a relevant masters degree is highly desirable.

This studentship is open to suitable UK/EU and International (i.e., outside the EU) applicants. Please note though that the award covers tuition fees at the UK/EU rate only. International applicants (and those not eligible to pay UK/EU tuition fees) must demonstrate at the time of their application that they can fund the difference in tuition fee rates.

The studentship is for full-time study only and is available for immediate start.

Informal Enquiries

Informal enquiries are welcomed - please contact:

• Dr Nir Piterman
• np183@le.ac.uk
• Tel. +44 (0)116 252 3813

Apply Now

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

There is no closing date for applications and the studentship will remain open until filled. However, early application is encouraged - the studentship will be awarded as soon as a suitable applicant is identified.

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

Postgraduate Research at the University of Leicester

The University of Leicester is one of the UK's leading universities, committed to international excellence through the creation of world changing research and high quality, inspirational teaching. In 2008/2009 we were named the Times Higher Education's University of the Year, with the judges describing us as "elite without being elitist".

• Our Research Reputation
• Our Research Community
• Our Facilities
• A Diverse and Exciting City
• Department of Computer Science Website