[isabelle] PhD and Post-Doc positions at Chalmers



Chalmers University of Technology CSE Department is hiring: 3 PhD
students and 1 Post-Doctoral researcher in formal methods and in
language-based security.

Those I hire (1 PhD student and 1 Post-Doc) are encouraged to work
with interactive theorem proving in higher-order logic using HOL4.
Feel free to contact me with questions regarding these positions.

* 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 internationally recognised for
its high-profile research track record and 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,
Chalmersâ Formal Methods group developed and maintains verification
tools such as the CakeML toolchain (https://cakeml.org/) and the HOL4
theorem proving system (http://hol-theorem-prover.org/), 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/), and LARVA.

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.