Por Tiago Ferreira (UCL).

Abstract: Modern software increasingly depends on the correct behaviour of computer networks and their underlying protocols. Yet, these systems are often developed and deployed without formal models or specifications, making their analysis and verification difficult.

Automata Learning is a principled approach to automatically recover formal models of opaque systems, with correctness guarantees. By systematically interacting with closed-box systems, such as network components or protocol implementations, we can infer accurate models of their behaviour at varying levels of abstraction, from individual servers to entire networks. 

In this talk we will see how automata theory provides the strong correctness foundations that make automata learning both rigorous and practical. I will discuss how these algorithms power PROGNOSIS, a tool used to enabled powerful verification techniques such as model checking and automated bug finding that exposed issues ranging from DoS vulnerabilities in globally deployed software, to design flaws in modern network protocols.

Time permitting, I will also touch on how symbolic techniques enable a novel algorithm for learning NetKAT programs, a DSL for network verification, and how machine learning methods can enhance the usability of automata learning in complex domains without compromising its formal guarantees.

Bio: Tiago Ferreira is a final-year PhD student in the Programming Principles, Logic, and Verification (PPLV) group at University College London, supervised by Professors Alexandra Silva and Peter O'Hearn. He holds a BSc (Hons) in Mathematical Computation from UCL and has previously interned at Galois. His research focuses on automata learning for lightweight formal methods, aiming to make these techniques practical and accessible to non-experts and fast-moving industries.