Research Projects

FuncTion

Programming errors which cause non-termination can compromise software systems by making them irresponsive. Notorious examples are the Microsoft Zune Z2K bug3 and the Microsoft Azure Storage service interruption. Termination bugs can also be exploited in denial-of-service attacks. Therefore, proving program termination is important for ensuring software reliability. The traditional method for proving termination is based on the synthesis of a ranking function, a well-founded metric which strictly decreases during the program execution. The goal of the project is the development of a static analyzer which automatically infers ranking functions and sufficient precondition for program termination by means of abstract interpretation.

Lyra

The Lyra research project is a long-term research effort to enhance the understanding and reliabilty of data-driven decision-making software. It aims ad developing new practical and accessible analyses and tools to reason about and provide rigorous guarantees of the behavior of data analytics, big data, machine learning, and deep learning applications.

Recent Publications

More Publications

. Static Analysis of Data Science Software. To appear in SAS, 2019.

Project

. MaxSMT-Based Type Inference for Python 3. In CAV, 2018.

PDF Code Project BibTeX Springer

Recent Talks

More Talks

What Programs Want: Automatic Inference of Input Data Specifications
Tuesday, April 2, 2019
Static Program Analysis for a Software-Driven Society
Monday, March 26, 2018
Static Program Analysis for a Software-Driven Society
Thursday, March 22, 2018

Software

ApronPy


Python Interface for the APRON Numerical Abstract Domain Library

FuncTion


Abstract Interpretation-based Static Analysis for (Conditional) Termination (and Other CTL Properties)

Lyra


Abstract Interpretation-based Static Analysis for Data Science Applications

Typpete


SMT-based Static Type Inference for Python 3.x

Contact