Posted: 27th January 2010
The goal of this project is to develop algorithms and tools for automated formal verification of low-level C programs that make use of shared-variable concurrency. In spite of extensive research on concurrent computation, almost all existing program analysis tools are limited to sequential programs or programs that communicate via some form of explicit message passing. However, shared-variable concurrency is the predominant form of concurrency in commercial environments, and tool support is in dire need. The project focuses on
- verification by means of automated summarisation of threads,
- identification of transactions, enabling partial-order reductions, and
- Craig interpolation to derive thread invariants.
Applications are invited for a DPhil studentship funded by the project within the Automated Formal Verification Group in the University of Oxford's Computing Laboratory. The studentships include full support towards college and university fees (for home/EU nationals), as well as maintenance of at least £13,290 per annum.
Candidates should meet the selection criteria for studying for a D.Phil at Oxford University Computing Laboratory:
Applications are made online and information about how to apply, including requirements and links to the online prospectus, colleges and university funding, is available from:
Please quote the following studentship codes on the application form:
- 10-COMP-DK-WEB (If you are applying from ComLab web pages)
- 10-COMP-DK-JOBS (If you are applying from jobs.ac.uk)
- 10-COMP-DK-FIND(If you are applying from findaphd.com)
The successful candidates are expected to start their DPhil by October 2010 at the latest and will be supervised by Dr. Daniel Kroening and/or Dr. Joel Ouaknine of the Verification Group.
Closing date for the DPhil Studentships will be: 31st May, 2010