[TYPES/announce] RA positions at Imperial

[Gardner, Philippa A]

[Sorry for multiple postings.] 

Four three-year RA positions are available at Imperial College London: 
two on JavaScript analysis and verification; and two on concurrency
verification. For candidates with exceptional experience, it may be
possible to appoint one position at a more senior level and extend the
appointment beyond the three years.

[We are also interested in excellent PhD students, see
http://www3.imperial.ac.uk/computing/phd for how to apply.]

JavaScript analysis and verification:

The two  RA positions are to work with Philippa Gardner and Sergio
Maffeis, with project partners Alan Schmitt and Arthur Charguéraud of
INRIA.

The aim is to develop a general-purpose verification infrastructure
for client-side web programs, certified by a Coq specification whose
automatically-generated reference interpreter will be validated to
industrial standards. The project is part of the National Research
Institute in Automated Program Analysis and Verification funded by
EPSRC in association with GCHQ, and hosted at Imperial with Gardner as
the Director.

Candidates should have an interest in web technologies and a strong
track record in some of: separation logics, Coq, verification tools,
and static or run-time analysis for security.

A preliminary web page for the project can be found at
http://jscert.org/

Concurrency Verification:

The two RA positions are to work with Philippa Gardner. 

The aim is to develop the fundamental theory of concurrency
verification, including the design of verification tools and the study
of real-world applications such as the C11 library,
java.util.concurrent and the POSIX file system. The project is part of
the EPSRC Programme Grant `REMS: Rigorous Engineering of Mainstream
Systems' with Cambridge (PI: Peter Sewell) and Edinburgh (Ian Stark).

Candidates should have an interest in concurrency verification and a
strong track record in some of: separation logics, linearizability,
weak memory, Coq, verification tools and concurrent
programming. Gardner is looking for two researchers whose research
spans the breadth of these areas, from theory through to practice.  In
particular, this project provides an exciting opportunity to work with
the Cambridge systems researchers.

For further details, see http://www-lrr.doc.ic.ac.uk/ca/ for Gardner’s
work on concurrency verification and
http://www.cl.cam.ac.uk/~pes20/rems/ for the overall REMS project.

Application Process:

The closing dates for applications are 31st May 2013. Please see the attachments
for further details. 

Best wishes,
Philippa

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Advert javascript FINAL VERSION.doc
Type: application/msword
Size: 27648 bytes
Desc: Advert javascript FINAL VERSION.doc
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20130417/e56fcd3e/attachment-0001.doc>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Advert concurrencyFINAL VERSION.docx
Type: application/vnd.openxmlformats-officedocument.wordprocessingml.document
Size: 6096 bytes
Desc: Advert concurrencyFINAL VERSION.docx
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20130417/e56fcd3e/attachment-0001.bin>