Abstract

Generating Proofs and Assessing Specifications for More Effective Formal Verification

Formal verification provides strong guarantees about software correctness, but two fundamental challenges remain: constructing proofs efficiently and ensuring that the specifications being verified adequately capture the intended behaviour. In this talk, we will briefly introduce the Software Reliability Lab (SR Lab) and its research activities. We will then explore two complementary research directions. First, we will present our work on using large language models and agents to automate proof synthesis in Rocq and reduce the effort required for formal verification. We will then introduce MutDafny, which uses mutation testing to assess the strength of formal specifications written in Dafny. Together, these projects illustrate how advances in proof automation and specification assessment can make formal verification more practical, effective, and trustworthy.

About

Alexandra Mendes is an Assistant Professor at the Faculty of Engineering of the University of Porto (FEUP), Portugal, and co-leads the Software Reliability Lab. She was previously a Visiting Researcher at Carnegie Mellon University through the CMU Portugal Program, hosted at the CyLab Security and Privacy Institute, and a visiting researcher at University College London (UCL), hosted by the CREST group. She is also a member of the Formal Methods Teaching committee. She received an Amazon Research Award in Automated Reasoning and the Luso-American Development Foundation (FLAD) Atlantic Security Award. Her research focuses on advancing software verification by developing tools and methods that make verification more accessible and practical for software developers. Her work has been published at leading software engineering conferences, including ICSE, FSE, ASE, and ISSTA. She has also served as a PC member for major events such as ICSE, ASE, and ISSTA, and currently serves on the OOPSLA and CAV program committees. She holds a PhD in Computer Science from the University of Nottingham (UK).

João F. Ferreira is an Associate Professor at the Faculty of Engineering of the University of Porto (FEUP), Portugal, and a researcher at INESC-ID. He co-leads the Software Reliability Lab, where his research focuses on improving software reliability through formal methods, automated reasoning, and artificial intelligence. His current research interests include AI-assisted proof synthesis, program verification, and reliable Infrastructure as Code. His work has been published at leading software engineering conferences, including ICSE, FSE, ASE, and ISSTA. He is a recipient of an Amazon Research Award and an ICSE 2025 Distinguished Paper Award. Before joining the University of Porto in 2025, he was a Visiting Researcher at Carnegie Mellon University through the CMU Portugal Program, and he held academic positions at Instituto Superior Técnico (University of Lisbon) and Teesside University (UK). He holds a PhD in Computer Science from the University of Nottingham (UK).

About Current Trends in Computer Science

This lecture is part of the Current Trends in Computer Science Lecture Series by the TU Wien Informatics Doctoral School, where renowned Guest Professors hold public lectures every semester. If you are studying with us, the lecture series can be credited as an elective course for students of master’s programs of computer science: 195.072 Current Trends in Computer Science. Additionally, you can join courses held by this year’s Guest Professors of our doctoral colleges and the TU Wien Informatics Doctoral School.

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.