[TYPES/announce] 2 Ph.D positions on formal methods available at the University of Oslo
Martin Steffen
msteffen at ifi.uio.no
Wed Feb 2 03:42:50 EST 2022
+-----------------------------------------+
2 Ph.D positions in
Formal Methods
available at the
Dept. of Informatics,
University of Oslo.
on the following two topics:
+-----------------------------------------+
1. Symbolic Execution
2. Formal Analysis for Concurrent Programs
+-----------------------------------------+
Deadline: 28. 02. 2022
+-----------------------------------------+
1. Positions
===========
Both position will be part of the research group on formal methods at
the Department of Informatics (IFI). The research group develops and
applies techniques for formal modelling and analysis in a range of
problem domains. As a research fellow in this research group, you will
be working in a friendly, stimulating and international research
environment with a number of PhD and postdoctoral fellows.
The position targeting symbolic execution is part of a project in
collaboration with TU Darmstadt (Germany) and CWI Amsterdam (the
Netherlands).
2. Qualification requirements, employment details & how to apply
================================================================
For detailed information about how to apply, formal application
requirements and expectations, terms of employment and wage etc., see the
web announcements:
- https://urldefense.com/v3/__https://www.jobbnorge.no/en/available-jobs/job/219729/phd-research-fellow-in-symbolic-execution__;!!IBzWLUs!AgdKWIDzGxGavuMTR89a4qy-LT9XzVgwF35Lm4RBiewBcEx7h5-ftN1eydpKToeFZ4gzQruGNy80Uw$
- https://urldefense.com/v3/__https://www.jobbnorge.no/en/available-jobs/job/219775/phd-research-fellow-in-formal-analysis-of-concurrent-systems__;!!IBzWLUs!AgdKWIDzGxGavuMTR89a4qy-LT9XzVgwF35Lm4RBiewBcEx7h5-ftN1eydpKToeFZ4gzQruWF9OzEA$
3. Contacts:
===========
- Einar Broch Johnsen (einarj at ifi.uio.no)
- Silvia Lizeth Tapia Tarifa (sltarifa at ifi.uio.no)
- Eduard Kamburjan (eduard at ifi.uio.no)
- Martin Steffen (msteffen at ifi.uio.no)
4. More details on the intended area of research of the two positions:
====================================================================
4.1. Symbolic Execution
~~~~~~~~~~~~~~~~~~~~~~
The planned PhD research is concerned with symbolic execution of
concurrent and distributed systems. Symbolic execution is an elegant,
well-established technique to analyse software, which allows different
executions to be explored systematically and efficiently. It is used
both for testing and verification of program behaviour, with
applications in, e.g., security, memory management and behavioural
correctness. However, symbolic execution is today largely restricted
to sequential software; the current techniques do not scale to
concurrent and distributed systems due to an exponential increase in
the size of the search space of possible executions, which stems from
the additional non-determinism inherent to concurrency. The idea of
the project proposal is to devise abstraction techniques that enable
us to tackle the state-space explosion which currently makes
concurrent programs out-of-bounds for symbolic execution. This is an
exciting position for candidates interested in topics such as software
verification, static analysis and formal modelling languages.
4.2. Formal Analysis of Concurrent Systems
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The planned PhD research aims to develop formal semantic-based
analysis methods for tackling modern concurrency abstraction and
memory models for multi-threaded programming languages and
systems. That also involves developing and using appropriate software
analysis and synthesis tools to ensure synchronisation-related
correctness properties, such as deadlock-freedom, sequential
consistency, functional determinacy or absence of information
leakage. The results from the theoretical investigations will be
encapsulated in programming libraries and analysis algorithms that fit
into the existing eco-systems of the chosen host languages.
Methodologically, the research will target mainly light-weight
verification methods, analysis methods and corresponding tools that
work automatically, without interactive user intervention. In
particular, type-based analyses and synthesis methods to check for
resource-consumption, conformance with interface specification, race
freedom, etc.
More information about the Types-announce
mailing list