[ecoop-info] 2 Ph.D positions on formal methods available at the University of Oslo

[Martin Steffen]

+-----------------------------------------+

    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://www.jobbnorge.no/en/available-jobs/job/219729/phd-research-fellow-in-symbolic-execution
  - https://www.jobbnorge.no/en/available-jobs/job/219775/phd-research-fellow-in-formal-analysis-of-concurrent-systems


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.