AuRoRa

Randomization is a fundamental concept in computer science. It enables algorithms to run, on average, 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 of Probabilistic Programs

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, co-PI: Alejandro Aguirre)

Prusti

Prusti is a program verifier developed primarily at ETH Zurich for the Rust programming language. It exploits Rust’s type system to automatically derive a core proof for, amongst others, memory safety. This reduces the overall verification effort for functional correctness, because basic properties do not have to be specified and proved manually.

Decision Procedures for Separation Logic

Separation logic is an extension of Hoare logic to write elegant rigorous proofs for heap manipulating programs. We developed techniques for formal reasoning about satisfiability, entailment, and other robustness properties of separation logic. These techniques have been implemented in collaboration with TU Wien in an open-source tool called HARRSH.

Attestor

Attestor is an open-source tool for model-checking Java programs operating on dynamic data structures. Its theoretical foundations are based on abstract interpretation and context-free graph grammars to describe underlying data structures. The analysis is fully automated, procedure-modular, and provides visual feedback to understand property violations.

Funding: German National Research Council (DFG, PIs: Joost-Pieter Katoen and Thomas Noll)