[ecoop-info] PhD and Post-Doc positions in formal methods and security

[Carlo A. Furia]

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/).