Seminar Details
2026-11-03 (14:00) : Reading Between The Lines of Code
At Euler building (room A.002)
Duration: 60 minutes
Organized by Mathematical Engineering
Speaker :
Elizabeth Polgreen (University of Edinburgh)
Abstract :
Formal verification is hard. It is even harder when you do not know what property you should be verifying.
People are notoriously bad at stating precisely what they want, and natural language is inherently ambiguous. As a result, the software, hardware and systems we rely on often come without usable specifications for formal verification. Even when specifications do exist, they are often insufficiently detailed for automated verification tools to prove the properties we care about. This gap is becoming increasingly important as AI-generated code enters the software and hardware ecosystem: we may be able to generate implementations faster than ever, but understanding what those implementations are supposed to do remains a core challenge.
In this talk, I will discuss our group’s attempts to close this gap through specification mining: automatically inferring the properties that are implicit in code, designs, and their behaviour. Drawing on classical program synthesis techniques as well as large language models, we are exploring methods for efficiently mining specifications for both hardware and software. Our aim is to reduce the manual burden of formal verification and, ultimately, to enable the verification of systems without requiring users to write formal specifications by hand.