[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
Advert javascript FINAL VERSION.doc
Description: Advert javascript FINAL VERSION.doc
Advert concurrencyFINAL VERSION.docx
Description: Advert concurrencyFINAL VERSION.docx
------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
