[Agda] Microsoft-funded PhD opportunity (software/ system verification)

[Tom Ridge]

Dear Colleagues,

I would be very grateful if you could bring the following advert to
the attention of potential applicants. Also, if anyone if interested
in the project, please do get in touch!

Thanks

Tom

--

Microsoft Research PhD studentship: Future Filesystems
======================================================

Project: Future filesystems: mechanized specification, validation,
implementation and verification of filesystems

Supervisors: Tom Ridge (with Andrew Kennedy at Microsoft Research)

Application deadline: 2013-06-02 (June 2nd)

PhD expected start date: 2013-10-01

We seek strong candidates for a Microsoft PhD studentship on "verified
filesystems". The PhD scholarship is fully funded for three years. The
project will be supervised by Tom Ridge at the Department of Computer
Science, University of Leicester, in collaboration with Andrew Kennedy
at Microsoft Research Cambridge.

Project description
-------------------

Filesystems are extremely important. Users depend on filesystems to
store their files whenever they hit "save". Businesses rely on databases
to store their data safely, and these databases in turn rely on the
filesystem.

Modern filesystems are designed to satisfy many complicated
requirements. As a result, implementations are beset with problems. The
implementation code is extremely complex, and almost inevitably contains
bugs. These bugs can and do lead to data corruption and loss.
Development time is very lengthy. Testing is also very lengthy and
costly, and does not guarantee to eliminate all bugs. It is often
unclear to application developers what guarantees a filesystem provides,
so that it becomes extremely difficult to write correct applications for
a given filesystem, let alone applications that are portable across
different filesystems.

In this project, we aim to tackle these problems by applying formal
methods techniques. We will specify the behaviour of existing
filesystems using higher-order logic (supported by the HOL4 theorem
prover). Further, we will implement a filesystem, and verify functional
correctness of the implementation with respect to the specification. We
are particularly interested in the behaviour of filesystems when the
host crashes. The project involves theoretical aspects (for example, we
are interested in understanding the dependencies that arise when
different filesystem operations execute; the project will also involve
extensive proofs, both informal and mechanized) but is focused on
applications of theory to real-world systems.

Background of applicant
-----------------------

Ideally the applicant should be a good programmer (with knowledge of one
of the main functional programming languages such as OCaml, Haskell, SML
etc), with background in semantics (particularly operational semantics),
theorem proving, and verification. The applicant must have a strong
interest in producing reliable systems.

Applicants should hold at least a good second-class honours degree or
equivalent in computer science (or a closely related discipline) and
have a good command of English. A masters degree may be an advantage,
but is not necessary.

Funding
-------

The Microsoft scholarship consists of an annual bursary for 3 years.
This studentship is fully funded (fees and stipend) for UK and EU
students. The stipend is up to 17,000 UK pounds. We welcome overseas
applicants, and would provide the equivalent of home/EU fees and
maintenance for a successful overseas candidate; the difference between
home/ EU fees and international fees (approx. 11,000 UK pounds per
annum) would need to be funded by the overseas applicant.

Environment
-----------

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.

Application process
-------------------

We encourage potential applicants who wish to express their interest in
the project to email Tom Ridge `tr61 (at) le.ac.uk` well before the
deadline.

The application process is via the University of Leicester. For further
details on the application process, see
<http://www2.le.ac.uk/study/research/funding/future-filesystems>

Further questions
-----------------

Please contact Tom Ridge `tr61 (at) le.ac.uk` if you have any further
questions.