PhD and Post-Doc positions in formal methods and security

The Software Technology Division of the Computer Science and Engineering
Department, Chalmers University of Technology is hiring:

2 PhD students and 1 Post-Doctoral researcher in formal methods and 1
PhD student in language-based security.

* Application deadline: 10 April 2016.

* Expected starting date: preferably around September 2016.

For details, including employment conditions and how to apply, see:

http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=3853
http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=3854
http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=3855


2 PhD student and 1 Post-Doctoral researcher position in Formal Methods:
------------------------------------------------------------------------

The Formal Methods group of Chalmers is an internationally recognised
research group with a high-profile research track record and an
extensive network of collaborators. The group's research focus are the
theoretical and practical aspects of rigorous software analysis and
verification, including techniques such as automated reasoning,
interactive theorem proving, runtime verification, automated test
generation, and program synthesis. In collaboration with other
researchers worldwide, Chalmer's Formal Methods group developed and
maintains verification tools such as KeY (http://www.key-project.org),
Vampire (http://vprover.org), ALIGATOR
(http://mtc.epfl.ch/software-tools/Aligator), the Eiffel Verification
Environment (http://se.inf.ethz.ch/research/eve/ and
http://comcom.csail.mit.edu/autoproof/), LARVA, the CakeML toolchain
(https://cakeml.org/) and the HOL theorem proving system
(http://hol-theorem-prover.org/).

We are looking for outstanding candidates with interest in pursuing
research in one or more of the following areas:

1. Automated program repair
2. Functional-correctness verification of software
3. Combining heterogeneous verification techniques
4. Synthesis of programs and specifications
5. Compiler correctness (for e.g. just-in-time compilation)

These positions will be supervised by Prof. Carlo A. Furia (1 PhD
student, research areas 1-4, see http://bugcounting.net) and
Prof. Magnus Myreen (1 PhD student and 1 Post-Doctoral researcher,
research areas 2-5, see http://www.cse.chalmers.se/~myreen/).


1 PhD student position in language-based security
-------------------------------------------------
The PhD students will join a high-profile group of researchers on
software security with a rich network of collaborators and visibility
across several research communities (security, programming languages,
and systems research). In collaboration with top universities,
researchers at Chalmers have developed some of the state of the art
tools for protecting users' private data in Haskell programs (e.g.,
LIO https://hackage.haskell.org/package/lio) as well as web browsers
(COWL http://cowl.ws/).

The position focuses on developing techniques to protect confidentiality
and integrity of users' data when manipulated by
untrusted code -- a pressing problem for the web as well as mobile
platforms. It is expected that the work carried out by the applicant
ranges from establishing new theoretical foundations to deploying
prototypes in production systems. We are looking for outstanding
candidates with background in either programming languages and/or
systems research interest in pursuing one or more of the following
topics:

1. Combining static and dynamic techniques to secure Haskell programs.
2. Leveraging hardware-level security components (e.g, Intel SGX and
ARM TrustZones) to provide security in depth, where private data
can be protected from the application level down to the low-level
physical layers.
3. Developing domain specific languages to express different kind of
security policies.

This position will be supervised by Prof. Alejandro Russo
(http://www.cse.chalmers.se/~russo/).