Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] PhD and Post-Doc positions at Chalmers


view this post on Zulip Email Gateway (Aug 22 2022 at 13:01):

From: Magnus Myreen <mom22@cam.ac.uk>
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.

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


Last updated: Mar 29 2024 at 08:18 UTC