Dominik Winterer

alt text 

Ph.D. Student
Department of Computer Science
ETH Zurich, Switzerland

Email: dominik.winterer@inf.ethz.ch
Office: CNB H 103.2

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, Dominik is developing tools for stress-testing SMT solvers in the Yin-Yang project.
Check out our twitter account @testsmtsolvers for most recent bug findings in Z3 and CVC4!


We have recently released our Yin-Yang framework. It is an umbrella release with both Semantic Fusion and OpFuzz from our PLDI and OOPSLA papers. The tool has already found 1,000+ bugs in Z3 and CVC4. Please check it out!

News

10-30-2020           Our SMT Solver testing framework YinYang has been officially released on GitHub.
09-31-2020           Our paper on Type-Aware Operator mutation was conditionally accepted at OOPSLA!
05-13-2020           Our paper on Semantic Fusion won a distinguished paper award at PLDI 2020!
05-12-2020           I'll be a student volunteer at PLDI 2020.

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

[Publications in AI Planning]

Teaching

Teaching Assistant at ETH Zurich

Teaching Assistant at University of Konstanz

Student Teaching Assistant at University of Freiburg

(Co-)supervised Theses

Services