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

I am a fifth-year Ph.D. student at ETH Zurich advised by Prof. Zhendong Su and a member of the AST lab since March 2019. I am interested in formal methods problems in Programming Languages and Software Engineering. Before my Ph.D. studies, I did undergraduate research in Automated Planning. In 2018, I received an MSc. in computer science from the University of Freiburg (Germany) and in the summer of 2017, I interned at IBM Research Yorktown Heights.
My primary research goal is to make SMT solvers more robust, reliable, and performant through principled, general automated testing techniques. My tools have found 1,700+ bugs in the flagship SMT solvers Z3 and CVC5; 500+ are critical soundness bugs.
From October 2023 to February 2024, I was interning in the Automated Reasoning Group of AWS where I applied and further developed testing techniques for SMT solvers in a real-world production setup.

News

Feb '24  I was invited to give talks at UPenn and Harvard!
Sep '23   I'll be interning in the Automated Reasoning Group of AWS in NY beginning October!
Aug '23   Invited to serve as Artifact Evaluation Co-Chair of ISSTA 2024!
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

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

Invited Talks

Service

Teaching

@ETH Zurich

@University of Konstanz

@University of Freiburg