PhD Position at Uni. Oslo: Formal Methods for Probabilistic Programs

by Einar Broch Johnsen, April 23, 2021

The main purpose of this PhD position is to investigate the applicability of symbolic execution techniques for probabilistic programs. Probabilistic programs are used to derive statistical information from uncertain data such as real-world observations. Symbolic execution is a technique for program analysis, based on executing programs with symbolic input values. This is an exciting position for candidates interested in combining logic and statistics with programming in their PhD research, and who have enjoyed topics such as foundations of programming languages, probability theory and statistics, executable models and operational semantics, formal methods and concurrency theory.

The main purpose of this PhD position is to investigate the applicability of symbolic execution techniques for probabilistic programs.

Probabilistic programs are used to derive statistical information from uncertain data such as real-world observations. Software systems which need to handle uncertain data can be found in, for example, security, robot control systems and machine learning algorithms. Probabilistic programming aims to make probabilistic data available to programmers.

Symbolic execution is a technique for program analysis, based on executing programs with symbolic input values. By doing so, this technique is able to systematically explore the different execution paths of a program for all input values. Symbolic execution is used for both software testing and software verification. In this project, we explore the concepts and applicability of symbolic execution for probabilistic programs.

The project will be executed in the context of the Formal Methods group at the department, which develops and applies techniques for formal modelling and analysis in a range of problem domains. Of particular relevance is our participation in REMARO, a European MSCA PhD training network on reliable robotic control systems. The project will be supervised by Prof. Einar Broch Johnsen and further involves international collaborators Prof. Andrzej Wasowski (IT-University of Copenhagen, DK), Prof. Alexandra Silva (University College London, UK) and Prof. Ina Schaefer (Technical University of Braunschweig, DE).

For more information, please contact Einar Broch Johnsen ([email protected])

The formal announcement and application procedure is explained here:
https://www.jobbnorge.no/en/available-jobs/job/202841/phd-research-fellowship-in-formal-methods-for-probabilistic-programs