Formal methods: from pie in the sky to industrial practice

Μέρα/Ώρα: Τετάρτη 4/12, ώρα 11πμ

Τόπος: Τ203, Κτίριο Τροίας

Διαδικτυακή παρακολούθηση μέσω Teams

Title:
Formal methods: from pie in the sky to industrial practice

Abstract:
Formal methods such as formal verification allow to prove software correctness under all cases, in contrast to testing. Research in the last 50 years or so, has succeeded in turning formal methods from "pie in the sky" to industrial practice. In this talk I will give an overview of the area, starting with "manual" formal verification (theorem proving), and continuing with automated formal verification (model checking). I will then present some of our current research in the areas of verification and synthesis of distributed protocols, using counterexample-guided techniques for inductive invariant inference and synthesis by sketching. I will end by sharing my thoughts on the current state of AI. The talk is for a broad audience and requires no background in formal methods.

Bio:
Stavros Tripakis is an Associate Professor of Computer Science at Northeastern University Boston. He received his Diploma in Computer Science from the University of Crete in 1992 and his Ph.D. in Computer Science at the Verimag Laboratory and Grenoble University in 1998. He has held positions at the University of California at Berkeley, at the French National Research Center CNRS, at Cadence Design Systems, and at Aalto University. His research interests are in the foundations of software and system design, formal methods, and cyber-physical systems. His H-index is 57.