Caterina Urban

Research Scientist (Chargé de Recherche)

École Normale Supérieure

I am looking for motivated PhD students and interns in the scope of the Lyra research project!

I am a member of the INRIA research team ANTIQUE (ANalyse StaTIQUE). Previously, I was a postdoctoral researcher at the Chair of Programming Methodology, led by Peter Müller at ETH Zurich. I completed my Ph.D. in Computer Science, working under the joint supervision of Radhia Cousot and Antoine Miné at École Normale Supérieure. I hold a Bachelor’s and a Master’s degree in Computer Science, both received with full marks and honors (summa cum laude) from the Università degli Studi di Udine.

My research interests span the whole spectrum of formal methods and aim at developing methods and tools to enhance the reliability of computer software and understanding complex software systems. My main area of expertise is static analysis based on abstract interpretation, which provides rigorous mathematical guarantees of the behavior of computer programs. I am currently engaged in a long-term research effort to enhance the understanding and reliability of data science software, which nowadays plays an increasingly important role in critical decision making in fields such as finance and medicine.

News

👥 I am a member of the SOAP 2020 program committee

👥 I am a member of the VSTTE 2020 program committee

👥 I am a member of the SAS 2020 program committee

🏰 I will be attending the Dagstuhl Seminar 20251 “Theoretical Advances and Emerging Applications in Abstract Interpretation”

👩🏼‍💻 I have been developing a Python interface for the APRON numerical abstract domain library. Contributions are welcome!

Interests

Static Program Analysis
Abstract Interpretation
Programming Languages
Data Science

Education

PhD in Computer Science, 2015

École Normale Supérieure, Paris, France
MSc in Computer Science, 2011

Università degli Studi di Udine, Udine, Italy
BSc in Computer Science, 2009

Università degli Studi di Udine, Udine, Italy

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

Caterina Urban, Maria Christakis, Valentin Wüstholz, Fuyuan Zhang. Perfectly Parallel Fairness Certification of Neural Networks. CoRR abs/1912.02499, 2019.

PDF Code Project BibTeX arXiv

Caterina Urban. Static Analysis of Data Science Software. In SAS, 2019.

PDF Project

Caterina Urban, Samuel Ueltschi, Peter Müller. Abstract Interpretation of CTL Properties. In SAS, 2018.

PDF Code Project Video BibTeX Springer FuncTion