profile_pic 

Dominik Winterer

Ph.D. Student
Department of Computer Science
ETH Zurich, Switzerland

Email: dominik.winterer@inf.ethz.ch
Office: CNB H 103.2

google_scholar twitter github

About

Dominik Winterer is a fourth-year Ph.D. student at ETH Zurich advised by Prof. Zhendong Su and a member of the AST lab since March 2019. He is interested in formal methods problems in Programming Languages and Software Engineering. Before his Ph.D. studies, Dominik did research in Automated Planning. In 2018, Dominik received an MSc. in computer science from the University of Freiburg (Germany). In the summer of 2017, Dominik interned at IBM Research NY, where he worked on top-k planning.
Currently, Dominik's primary research goal is to make SMT solvers more robust, reliable, and performant through principled, general automated testing techniques with a potential to be applicable beyond SMT solvers. His tools have found 1,500+ bugs in the flagship SMT solvers Z3 and CVC5; 400+ are critical soundness bugs.
Dominik is the organizer of the Future of Software Seminar at ETH Zurich.

News

Jan '23   I'll be giving an invited talk at UCSC's LSD seminar
Dec '22  Invited to serve on the Program Committee of ICSE '24 (demo track)!
Nov '22   I'll be giving an invited talk at USC Software Seminar!
Sep '22   Invited to serve on the program committee of MET2023 collocated with ICSE
Sep '22   I'll be giving a talk at KIT's research seminar on formal methods
Aug '22  Our work on Finding Incompleteness Bugs in SMT solver got accepted at ASE '22. Congrats Mauro!
Jun '22  Invited to visit Paderborn University and give a talk
May '22  Invited to the Program Committee of SYNASC 2022
Apr '22   We won an Amazon Research Award for Project YinYang for SMT Solver Testing!
Apr '22   Invited to the Heidelberg Laureate Forum!
Mar '22   Invited to the Dagstuhl seminar on Research methods in Software Engineering
Feb '22   I will be organizing the Future of Software Seminar at ETH

Research

symbol 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 (all)

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

  2. 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.

  3. 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.

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

    award Distinguished Paper Award

    Invited to TOPLAS special issue on PLDI '20

Supervised Students

Awards and Grants

Selected Talks

Service

Teaching

@ETH Zurich

@University of Konstanz

@University of Freiburg