In the last 15 years, research in formal methods and verification has finally started to deliver practical techniques that are applicable to realistic software and bring tangible benefits to developers. In this talk, I will discuss what set off this "new wave" of practical formal methods, and how my research contributed to it. Guided by the engineering idea of finding interesting trade-offs between the effort required to apply an approach and the benefits it brings, I will present rigorous techniques, from automated program repair to full functional correctness verification, that have been successfully applied to realistic object-oriented software to improve its correctness and quality.

Carlo A. Furia is an associate professor in the Formal Methods/Software Technology Division of Chalmers University of Technology. His research interests center around developing rigorous techniques and tools to analyze and improve the quality, correctness, and reliability of software and systems. He is active in various software engineering (ICSE, ASE, ISSTA, TSE), formal methods (FM, iFM, SEFM, FAOC), and verification (TACAS, RV, VSTTE, STTT) communities and venues. Before joining Chalmers, he spent around seven years working as senior researcher in the Chair of Software Engineering at ETH Zurich. He has a PhD from the Politecnico di Milano.