USI - Email

Archive / INF Seminars / INF_2025_02_27_DominikWinterer

USI - Email

	Formal Methods Engineering (FME): Towards More Mature Formal Methods

Chair: Prof. Paolo Tonella

Thursday

27.02

D1.13

16:30 - 17:30


	Dominik Winterer ETH Zurich

Abstract: Software pervades all aspects of our personal and professional lives. But unfortunately, dangerous bugs still occur regularly, causing tremendous harm. Formal Methods are mathematical techniques to prevent dangerous bugs in software. Despite decades of research with substantial breakthroughs, Formal Methods have not yet been widely adopted. One major reason is that Formal Methods tools are often immature, i.e., unreliable, unstable, slow, or not user-friendly.
I propose Formal Methods Engineering (FME), a dedicated discipline for making Formal Methods more reliable, stable, performant, and usable. I will first present my research body on solidifying SMT Solvers-one of the most powerful Formal Methods foundational for many others. I will present a series of techniques uncovering 1,800+ bugs in SMT solvers, 1,300 of which were fixed, and 300+ critical soundness bugs. I will close with an outline of my vision for Formal Methods Engineering.

Biography: Dominik Winterer is a postdoctoral researcher at ETH Zurich, working at the intersection of Programming Languages, Software Engineering, and Formal Methods. His vision is to develop Formal Methods Engineering to help make Formal Methods more practical and widely adopted. During his Ph.D., Dominik solidified Satisfiability Modulo Theory (SMT) Solvers, uncovering 1,800 bugs, 1,300 of which were fixed. His research was awarded several prestigious distinctions, including an ACM Distinguished Paper Award at PLDI ‘20 and an Amazon Research Award (Co-PI) in 2022.

*************************
In February 2019, the Software Institute started its SI Seminar Series. Every Thursday afternoon, a researcher of the Institute will publicly give a short talk on a software engineering argument of their choice. Examples include, but are not limited to novel interesting papers, seminal papers, personal research overview, discussion of preliminary research ideas, tutorials, and small experiments.

On our YouTube playlist you can watch some of the past seminars. On the SI website you can find more details on the next seminar, the upcoming seminars, and an archive of the past speakers.