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

second profile pic

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. Currently, his main research goal is making SMT solvers more robust, reliable and performant through principled, general automated testing techniques with a potential to be applicable beyond SMT solvers.
Before his Ph.D. studies, Dominik did undergraduate research in Automated Planning. In 2018, Dominik received a MSc. in computer science from University of Freiburg (Germany). In summer 2017, Dominik interned at IBM Research Yorktown Heights where he worked on top-k planning.
Dominik is the organizer of the Future of Software Seminar at ETH Zurich.

News

Jul '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,560 (total) / 1,061 (fixed)]
[Reports: YinYang, OpFuzz,TypeFuzz]

yinyang  shield

Selected Publications (all)

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

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

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

Invited Talks

Service

Teaching

@ETH Zurich

@University of Konstanz

@University of Freiburg