Dominik Winterer Ph.D. Student Department of Computer Science ETH Zurich, Switzerland Email: dominik.winterer@inf.ethz.ch Office: CNB H 103.2

About

Dominik Winterer is a Ph.D. student advised by Prof. Zhendong Su at ETH Zurich and a member of the AST lab. He is interested in formal methods problems in Programming Languages and Software Engineering. Before his Ph.D. studies, Dominik did undergraduate research in Automated Planning (branch of symbolic AI). Currently, he is researching techniques for testing SMT solvers and making them more reliable.

Testing SMT Solvers

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. (more details)

[Z3/CVC4 Bugs: 1,500 (total) / 989 (fixed)]
[Reports: Semantic Fusion (YinYang), Type-aware Mutation (OpFuzz)]

 

Publications

1. Generative Type-Aware Mutation for Testing SMT Solvers
   Jiwon Park, Dominik Winterer, Chengyu Zhang, Zhendong Su
   In Proceedings of SPLASH/OOPSLA 2021 (conditionally accepted)
   

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.
   

   PLDI Distinguished Paper Award

   Invited to TOPLAS special issue on PLDI '20

Supervised Students

• Mauro Bringolf (Master thesis, ongoing)

• Jiwon Park (Bachelor thesis, completed)

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

Awards and Grants

• Google Open Source Peers Bonus 2021

• PLDI '20 Distinguished Paper Award

• IJCAI '16 Travel Grant

Services

• Reviewer/Judge Student Research Competition: OOPSLA ’21

• Artifact Evaluation Committee Member: ISSTA ’21

• Reviewer: JAIR '17, AAAI '20, AAAI '21

Teaching

@ETH Zurich

• Software Engineering, Spring 2021 (Head TA)

• Data Modelling and Databases, Spring 2020
  

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

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

@University of Konstanz

• Decision Procedures, Fall 2018

@University of Freiburg

• Model Checking, Fall 2016
  

• Theoretical Computer Science, Fall 2016