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

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

PDF Code Project BibTeX Springer

. Permission Inference for Array Programs. In CAV, 2018.

PDF BibTeX Springer

Recent Talks

More Talks

Static Program Analysis for a Software-Driven Society
Tuesday, March 26, 2019 10:15 AM
Static Program Analysis for a Software-Driven Society
Friday, March 22, 2019 11:00 AM



Python Interface for the APRON Numerical Abstract Domain Library


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


Abstract Interpretation-based Static Analysis for Data Science Applications


SMT-based Static Type Inference for Python 3.x