Headshot of Dominik Winterer

Dominik Winterer

Lecturer in Cyber Security — Formal Methods Engineering Lab

University of Manchester · Kilburn 2.81, Oxford Rd, M13 9PL, UK · dominik.winterer@manchester.ac.uk

I am an Assistant Professor (eq. UK: Lecturer) in Cyber Security 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 goal is best characterized as Formal Methods Engineering: making Formal Methods—mathematically rigorous methods for bug prevention—more practical, widely adopted, and resilient against AI.

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.

Teaching

  • COMP38412 Cybersecurity: Principles and Secure Software Systems, 2026-2027 (Unit Lead)
  • COMP63342 Software Security, Spring 2026 (Co-teaching)
  • COMP23311 Software Engineering, Fall 2025 (Co-teaching)

Earlier teaching, before Manchester »

Team

  • Lu Maltsis (Ph.D. student, Jan 2026 – )
    • Co-supervisor: Lucas Cordeiro
  • Kareem Seifo (Ph.D. student, Oct 2026 – )
    • Co-supervisor: Suzanne Embury
  • Andrei Zhukov (external MSc. thesis, completed Mar 2026)

Earlier supervised students, before Manchester »

Research Projects

CAST

Commit-Aware Solver Testing (CAST) continuously tests SMT solvers: every new commit is automatically built and fuzzed against a reference solver, so bugs are caught as soon as they’re introduced rather than long after the fact. The goal of CAST is to make continuous, automated bug-hunting a routine part of maintaining an SMT solver, turning testing from an occasional effort into an always-on safety net.

CAST stars CAST version

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.

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

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

Invited Talks

  • Formal Methods and Beyond: Finding and Fixing Bugs Through Domain-Specific Techniques
    TU Nuremberg, May 2026
  • Formal Methods Engineering: Toward Reliable Software Engineering
    Cornell & UT Austin SE Seminar (virtual), Dec 2025
    MPI-SP Sparkling Series, Apr 2025
    USI Lugano Software Seminar Series, Feb 2025
    UC Riverside (faculty interview), Jan 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