[TYPES/announce] PhD positions on formal methods and program analysis available at the University of Oslo

[Martin Steffen]

     Ph.D position in                                    
                                                                        
      Formal Methods                                       
                                                                         
     available at the                                      

  Dept. of Informatics,

   University of Oslo.                        
                                                                         
 on the topic
                                                                         
+--------------------------------------+                      
Formal Analysis for Concurrent Programs                     
+--------------------------------------+                    

Deadline: 31st August 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 announcement:

  - https://urldefense.com/v3/__https://www.jobbnorge.no/en/available-jobs/job/229366/phd-research-fellow-in-formal-analysis-of-concurrent-systems__;!!IBzWLUs!QblT0_RD5EcESP8aW7ut1fwRXW-rdTA-GPZNzl5zvSxH8BC9brXiKIw2gItJG9ySAqX2H50pKccj3tfWGWkDegKaBEEMsC3h1g$ 

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.