alt text 

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 on testing SMT solvers and making them more reliable.

Testing SMT Solvers

alt text 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: 1306 (total) / 805 (fixed)]
[Reports: Semantic Fusion (YinYang), Type-aware Mutation (OpFuzz)]

 

Publications

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

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

Awards and Grants

Services

Teaching

@ETH Zurich

@University of Konstanz

@University of Freiburg