Research
Research
This page lists current and previous research projects and software tools in which we have been involved.
Automated Reasoning about Randomized Algorithms (AuRoRa)
Randomization is a fundamental concept in computer science. It enables algorithms to run, on aver- age, faster and more resource-efficient than their deterministic counterparts, is essential in cryptography, and ensures fairness in distributed applications, such as electronic elections. In artificial intelligence, randomization expresses uncertainty, for example about the possible moves of a robot in difficult environments given limited sensor capabilities. Unfortunately, randomization is also the source of subtle bugs that are difficult to reproduce and counterintuitive to humans.
Project AuRoRa (Automated Reasoning about Randomized Algorithms) aims at improving the state of the art in automated verification of randomized systems by (1) developing novel intermediate verification languages for reasoning about quantitative properties of probabilistic programs and (2) exploring approaches for automating the building blocks of those languages.
Funding: Independent Research Fund Denmark (DFF project 1)
Automated Sensitivity Analysis
Sensitivity measures how much program outputs vary when changing inputs. In this project, we explored novel methodologies for specifying and verifying sensitivity properties of probabilistic programs such that they (a) are comprehensible to everyday programmers, (b) can be verified using automated theorem provers, and (c) cover properties from the machine learning and security literature.
Funding: Digital Research Centre Denmark (DIREC), collaboration with Alejandro Aguirre.
See also: https://direc.dk