Dominik Winterer Postdoctoral Researcher Automated Reasoning & Verification Group Department of Computer Science ETH Zurich, Switzerland Email: dominik.winterer@inf.ethz.ch Office: CNB H 108 I am on the academic job market!

About

I am a postdoctoral researcher at the Institute for Programming Languages and Systems at ETH Zurich. I will be working with Prof. Michalis Kokologiannakis. I got my Ph.D. from ETH Zurich advised by Prof. Zhendong Su, and was a member of the AST lab from March 2019 to September 2024.

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. 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, 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,800+ bugs in the flagship SMT solvers Z3 and CVC5; 500+ are critical soundness bugs.

News

Research Projects

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,825 (total) / 1,333 (fixed)] [Reports: YinYang, OpFuzz,TypeFuzz, Janus]

Selected Publications (all)

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

• Heidelberg Laureate Forum 2022

• Amazon Research Award Fall 2021(Co-PI)

• Google Open Source Peers Bonus 2021 (for yinyang)

• Invited to ACM TOPLAS Special Issue

• ACM Distinguished Paper Award (PLDI '20)

• IJCAI '16 Travel Grant Award

Supervised Students

• Pasquale Jordan (MSc. thesis, ongoing)

• Andrei Zhukov (Practical work, ongoing)

• Thea Kjeldsmark (Intern, completed)

• Luis Maltsis (Bachelor thesis, completed)

• Vince Szabo; (Intern, external thesis, completed)

  • POPL '24 SRC paper
  • first author on work on compilation hardness of PLs [preprint]

• Marc Andriu Carigiet (Bachelor thesis, completed)

• Michael Mörschell (Bachelor thesis, completed) → MSc. student @ETH Zurich

• Jiwon Park (Bachelor thesis + Internship, completed)   → Ph.D. student @UC Berkeley

  • 2nd place@FSE '21 SRC
  • Co-first author of OOPSLA '21 paper

• Mauro Bringolf (Master thesis, completed) → Software Engineer @ University of St. Gallen Digitec Galaxus

  • First author of ASE'22 paper

• Dylan J Wolff (Master thesis, completed) → Ph.D. student @National University of Singapore

  • POPL '21 SRC paper

• Altin Alickaj (Practical work, completed)   → Oracle labs

Invited Talks

• Solidifying SMT Solvers Through Automated Testing
  @Harvard PL Seminar. Mar 2024.

• Solidifying SMT Solvers Through Automated Testing
  @UPenn PLClub. Feb 2024.

• Directed Testing of a String Solver
  @Amazon Webservices, Feb 2024.

• Solidifying SMT Solvers
  @UC Berkeley Programming Systems Seminar. Jan 2024.

• Finding 1,700+ Bugs in the SMT Solvers Z3 and CVC5 in Three Years.
  @UCSC LSD Seminar. Feb 2023.

• Finding 1,700+ Bugs in the SMT Solvers Z3 and CVC5 in Three Years.
  @USC Software Seminar. Nov 2022.

• Finding 1,700+ Bugs in the SMT Solvers Z3 and CVC5.
  @KIT Research Seminar Formal Methods. Sep 2022.

• Finding 1,500+ Bugs in the SMT Solvers Z3 and CVC5.
  @Paderborn University. Jun 2022.

• Finding 1,000+ Bugs in the SMT solvers Z3 and CVC4.
  @CEA List at Paris Saclay. Feb 2021.

Service

• Reviewer TOSEM '24

• Artifact Evaluation Co-Chair: ISSTA 2024

• Program Committee of the ICSE 2024 (Demonstrations Track)

• Program Committee Member: AAAI '20, AAAI '21, SYNASC '22, MET '23

• Journal Reviewer JAIR '17, TSE '21

• Reviewer/Judge Student Research Competition: OOPSLA '21

• Artifact Evaluation Committee Member: ISSTA '21, POPL '21, PLDI '22

• SIGPLAN-M Longterm mentoring (Oct '21 - now)

Teaching

@ETH Zurich

• Algorithms and Data structures, Spring 2024

• Formal Methods and Functional Programming, Spring 2022

• Software Engineering, Spring 2021 (Head TA)

• Data Modelling and Databases, Spring 2020, 2023

• Research Topics in Software Engineering, Spring 2020, 2021, 2022, Fall 2020
  

• Compiler Design, Fall 2019, 2020, 2021 (Head TA)
  

@University of Konstanz

• Decision Procedures, Fall 2018

• Software Engineering, Fall 2018

@University of Freiburg

• Model Checking, Fall 2016
  

• Theoretical Computer Science, Fall 2016