Home Original page

Dominik Winterer: Home

About

I am an Assistant Professor (Lecturer) at the University of Manchester, where I 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 Formal Methods, mathematically rigorous methods for bug prevention, more 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

  • Dec 2025 Excited to be chairing the Student Research Competition at ASE ‘26!
  • Aug 2025 Excited to be invited to the Program Committee of PLDI ‘26!
  • Aug 2025 I was invited to speak at Cornell & UT Austin’s joint SE seminar!
  • Jul 2025 I was a guest in the Disseminate: The Computer Science Research Podcast by Jack Waudby!
  • Jul 2025 Excited to be on the Program Committee of Euro S&P ‘26!
  • May 2025 🎉 I am joining the University of Manchester as a Lecturer (Assistant Professor) in September. I’ll be leading the Formal Methods Engineering Lab. I’m hiring!
  • Mar 2025 Excited to be on the Program Committee of FUZZING ‘25!
  • Feb 2025 Excited to be on the Program Committee of ASE ‘25!

Dissertation

Solidifying Modern SMT Solvers

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

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.

Enumerative Testing

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.

ET stars

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

University of Manchester
ETH Zurich

Invited Talks

  • Formal Methods Engineering: Toward Reliable Software Engineering
    MPI-SP Sparkling Series, Apr 2025
    USI Lugano Software Seminar Series, Feb 2025
  • Solidifying SMT Solvers through Automated Testing Techniques
    Harvard PL Seminar, Mar 2024
    UPenn, PLClub, Feb 2024
    UC Berkeley, Programming Systems Seminar, Jan 2024
  • Directed Testing of a String Solver
    Amazon Webservices, Feb 2024
  • Finding 1,700+ Bugs in the SMT Solvers Z3 and CVC5
    UCSC LSD Seminar (virtual), Feb 2023
    USC Software Seminar (virtual), Nov 2022
    KIT Research Seminar Formal Methods, Sep 2022
    Paderborn University, Jun 2022
    CEA List at Paris Saclay (virtual), Feb 2021

Service

Teaching

@ETH Zurich @University of Konstanz @University of Freiburg