Emanuele D'Osualdo

Researcher in Computer Science

Research Positions

I am looking for enthusiastic and motivated students and postdocs to join my group at the University of Konstanz. We currently offer:

  • 1 PhD position:
    Full time (4 years)
    Salary: E 13 TV-L 100%

  • 1 Postdoc position:
    Full time (2 years + extensions)
    Salary: E 13 TV-L 100%

Topics

Our group focuses on formal verification techniques, for mainly two domains: probabilistic programs, and concurrent programs.

Verification of probabilistic programs

Our recent paper on the logic called Bluebell showed a promising approach to unify and extend various abstractions used for probabilistic reasoning.

This work opens a number of research directions:

  • Generalizations of the model
  • Mechanization in Rocq/Iris
  • Applications to verification of cryptographic protocols
  • Automatic proof search
  • Extensions to handle Quantum programs

Verification of concurrent systems

Our group studies proof techniques for the compositional analysis of concurrent system through two main tools: concurrent separation logic (e.g. Iris), and types.

For example, the TaDA Live logic provided an expressive compositional way to reason about fine-grained concurrent algorithms:

On the types side, session types provide a nice compositional abstraction for protocols in concurrent systems. We explored connections with separation logic through Curry-Howard isomorphisms:

We are also working on Multi-party Session Types in ongoing work with Felix Stutz.