[TYPES/announce] Ph.D position on formal methods available @ University of Oslo (short deadline)
Martin Steffen
msteffen at ifi.uio.no
Wed Mar 23 10:07:50 EDT 2022
+-----------------------------------------+
Ph.D position in
Formal Methods
available at the
Dept. of Informatics,
University of Oslo.
on the topic
+--------------------------------------+
Formal Analysis for Concurrent Programs
+--------------------------------------+
Deadline: 08. 04. 2022
1. Position
===========
The 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.
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/222897/phd-research-fellow-in-formal-analysis-of-concurrent-systems__;!!IBzWLUs!FPggx67PTjENQl-UxY3_A1TpO3eJYtOvN9_w60oLr9JWoF1KI3vQ8V1a34G7jZ4BsBd96oLLA4c0Qg$
3. Contacts:
===========
- Martin Steffen (msteffen at ifi.uio.no)
- Einar Broch Johnsen (einarj at ifi.uio.no)
4. More details on the intended area of research
================================================
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