Dominik Winterer

Incoming Lecturer (Assistant Professor)
Formal Methods Engineering Lab
Systems and Software Security Group
Department of Computer Science
University of Manchester, United Kingdom
Email: dominik.winterer@inf.ethz.ch
domwinterer@gmail.com


I am hiring! Looking for PhD students 👩‍🎓👨‍🎓, interns 👩‍💻👨‍💻, and visitors 🧳🧑‍🤝‍🧑 to join the Formal Methods Engineering Lab

About

I am an incoming Lecturer (Assistant Professor) at the University of Manchester starting September 2025, where I will lead the Formal Methods Engineering Lab. I completed my Ph.D. and PostDoc at ETH Zurich, and before that, my MSc at the University of Freiburg in Germany. I also did research internships at the Automated Reasoning Group at AWS and at IBM Research in the United States.

My research aims to establish Formal Methods Engineering—a new discipline focused on making mathematically rigorous methods for bug prevention practical and widely adopted. As a first step, I led one of the largest academic bug-hunting campaigns to date, uncovering over 1,800 bugs and enabling more than 1,300 fixes in SMT solvers , which are foundational tools in Formal Methods.

News

Dissertation

Solidifying Modern SMT Solvers

Satisfiability Modulo Theory (SMT) solvers are among the most powerful and mature formal methods. They are foundational in software research and industry—for example, AWS uses them to verify cloud services. SMT solvers solve NP-hard problems and build trust through proof, making correctness and performance crucial, especially in safety- and security-critical domains. Though long trusted, SMT solvers’ reliability had not been thoroughly tested. This thesis challenges that trust through five approaches to improve solver correctness and performance The first, Semantic Fusion, validates SMT solver correctness and revealed dozens of soundness bugs in Z3 and CVC4. Next, Type-Aware Operator Mutation, a simple but highly effective method, uncovered 1,254 bugs, including soundness bugs across nearly all theories. To improve upon this, Generative Type-Aware Mutation found 322 more bugs, including long-standing ones in CVC4. Janus targets incompleteness bugs, while Grammar-based Enumeration (ET) tackles correctness and performance. ET also helps track SMT solver evolution. Across five years, we found 1,825 unique bugs (483 soundness), with 1,333 fixed. This thesis has advanced the hardening of formal methods.

Research Projects

Project Yin-Yang for SMT Solver Testing

Satisfiability Modulo Theory (SMT) solvers are foundational tools for many subareas of computer science, including formal verification, programming languages, and software engineering. Their reliability and robustness are crucial, especially for the safety-critical domains. However, effectively validating SMT solvers has been a longstanding challenge. The goal of Project Yin-Yang is to develop novel, effective, practical methods and techniques to help make SMT solvers more reliable, powerful, and usable.

[Z3/CVC4/5 Bugs: 1,677 (total) / 1,244(fixed)]
[Reports: YinYang, OpFuzz,TypeFuzz, Janus]

yinyang  shield

Enumerative Testing

The enumerative testing framework ET exhaustively enumerates test cases based on a context-free grammar. It will generate small test cases first exploiting the small-scope hypothesis which states that “most bugs in software trigger on small inputs”. Testing with small test cases has many unique benefits: tiny bug triggers, bounded guarantees, the ability to measure the evolution of a software.

Selected Publications


  1. Validating SMT Solvers for Correctness and Performance via Grammar-based Enumeration
    Dominik Winterer, Zhendong Su
    In Proceedings of SPLASH/OOPSLA 2024

      ⭐ Bounded Validation of the SMT Solvers Z3 and cvc5

  2. Finding and Understanding Incompleteness Bugs in SMT Solvers
    Mauro Bringolf, Dominik Winterer, Zhendong Su
    In Proceedings of ASE 2022   [slides / tool]

  3. Generative Type-Aware Mutation for Testing SMT Solvers badge_available badge_reusalbe badge_functional
    Jiwon Park*, Dominik Winterer*, Chengyu Zhang, Zhendong Su
    In Proceedings of SPLASH/OOPSLA 2021   [slides / video abstract]
    * Both authors contributed equally.

  4. On the Unusual Effectiveness of Type-Aware Mutations for Testing SMT Solvers
    Dominik Winterer*, Chengyu Zhang*, Zhendong Su
    In Proceedings of SPLASH/OOPSLA 2020   [slides / video abstract]
    * Both authors contributed equally.

      ⭐ 1,000+ bugs in the SMT Solvers Z3 and CVC4

  5. Validating SMT Solvers via Semantic Fusion
    Dominik Winterer*, Chengyu Zhang*, Zhendong Su
    In Proceedings of PLDI 2020   [slides / video abstract]
    * Both authors contributed equally.

    🏆 ACM Distinguished Paper Award

    ⭐ Invited to ACM TOPLAS Special Issue

Awards and Grants

Supervised Students

Invited Talks

Service

Teaching

@ETH Zurich @University of Konstanz @University of Freiburg

last updated: May 22, 2025