Projects

The ForML project investigates the use of abstract interpretation and counterexample-guided abstraction refinement with the purpose of efficiently answering queries about semantic properties of machine learning models such as robustness, fairness, and explainability. We also aim to formally verify existing and novel algorithms for answering such queries, and to derive certified implementations.

The goal of SAIF is to use the vast knowledge accumulated over decades in formal methods to rethink them and address the novel safety concerns raised by machine learning-based systems. Through the synergy of a diverse consortium with complementary expertise, we aim to bring society closer to a state where it can benefit from achievements in machine learning without suffering undue consequences.

[…page under construction…]

The goal of the Libra project is to develop new analyses and tools to reason about and certify fairness of decision-making software.

The Lyra research project is a long-term research effort to enhance the understanding and reliabilty of data science 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.

The goal of the FuncTion project was the development of a static analyzer which automatically infers ranking functions and sufficient precondition for program termination (and other liveness properties) by means of abstract interpretation.