Research Projects


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.


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

. Perfectly Parallel Fairness Certification of Neural Networks. CoRR abs/1912.02499, 2019.

PDF Code Project BibTeX arXiv

Recent Talks

More Talks

Static Analysis of Data Science Software
Wednesday, October 9, 2019
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



Python Interface for the APRON Numerical Abstract Domain Library


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


Perfectly Parallel Abstract Interpretation-based Fairness Certification for Neural Networks


Abstract Interpretation-based Static Analysis for Data Science Applications


SMT-based Static Type Inference for Python 3.x