Valentin Wüstholz

   

Valentin is a postdoctoral researcher at ETH Zürich in the group of Prof. Dr. Peter Müller. He has been contributing to several program analysis tools: Boogie, Clousot, Dafny, and Spec#.

After obtaining his Ph.D. from ETH Zürich (advisor: Prof. Dr. Peter Müller) in 2015, he was a postdoctoral researcher at the University of Texas at Austin in the group of Prof. Dr. Işil Dillig and a visiting researcher at Microsoft (Redmond, WA).

As a Ph.D. student and research assistant at ETH Zürich he has been working on the design and development of a practical tool architecture for analyzing programs collaboratively using static and dynamic tools.

He has been working with Prof. Dr. Rustan Leino as a research intern at Microsoft Research (Redmond, WA) and has been a software engineering intern at Google (Santa Monica, CA). He received a Master's degree (2009, with distinction) and a Bachelor's degree (2008) in Computer Science from ETH Zürich.

Publications (BibTeX, DBLP)

  • Valentin Wüstholz, Oswaldo Olivo, Marijn Heule, Işil Dillig: Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions. In Proceedings of the 23nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2017. (to appear)
  • Maria Christakis, Valentin Wüstholz: Bounded Abstract Interpretation. In Proceedings of the 23rd International Static Analysis Symposium (SAS), 2016.
  • Maria Christakis, Peter Müller, Valentin Wüstholz: Guiding Dynamic Symbolic Execution toward Unverified Program Executions. In Proceedings of the 38th International Conference on Software Engineering (ICSE), 2016. (ACM SIGSOFT Distinguished Paper Award)
  • Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz: Integrated Environment for Diagnosing Verification Errors. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016.
  • K. Rustan M. Leino, Valentin Wüstholz: Fine-grained Caching of Verification Results. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV), 2015.
  • Maria Christakis, Peter Müller, Valentin Wüstholz: An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer. In Proceedings of the 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015. (invited for journal special issue)
  • Maria Christakis, Peter Müller, Valentin Wüstholz: Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations. In Proceedings of the 12th International Conference on Software Engineering and Formal Methods (SEFM), 2014. (invited for journal special issue)
  • K. Rustan M. Leino, Valentin Wüstholz: The Dafny Integrated Development Environment. In Proceedings of the 1st Workshop on Formal Integrated Development Environment (F-IDE), 2014.
  • Maria Christakis, Peter Müller, Valentin Wüstholz: Collaborative Verification and Testing with Explicit Assumptions. In Proceedings of the 18th International Symposium on Formal Methods (FM), 2012.
  • Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß: The 1st Verified Software Competition: Experience Report. In Proceedings of the 17th International Symposium on Formal Methods (FM), 2011. (Best Paper Award)

Technical Reports and Theses

  • Valentin Wüstholz: Partial Verification Results. Ph.D. Thesis, ETH Zürich, 2015. [PDF]
  • Maria Christakis, Peter Müller, Valentin Wüstholz: Guiding Dynamic Symbolic Execution toward Unverified Program Executions. Technical Report, ETH Zürich, 2015. [PDF]
  • Maria Christakis, Peter Müller, Valentin Wüstholz: An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer. Technical Report, ETH Zürich, 2014. [PDF]
  • Valentin Wüstholz: Encoding Scala Programs for the Boogie Verifier. Master's Thesis, ETH Zürich, 2009. [PDF]

Professional Activities

  • ICSE 2017, OOPSLA 2016, PLDI 2016: Reviewer
  • ECOOP 2014: Artifact Evaluation Committee

Teaching

Valentin has been a teaching assistant for the following courses:

  • Software Engineering Seminar (Prof. Dr. Peter Müller, ETH Zürich): Fall 2014
  • Software Architecture and Engineering (Prof. Dr. Peter Müller and Prof. Dr. Martin Vechev, ETH Zürich): Spring 2014
  • Introduction to Programming (Prof. Dr. Bertrand Meyer, ETH Zürich): Fall 2013, Fall 2012, Fall 2011, Fall 2010
  • Software Architecture and Engineering (Prof. Dr. Martin Vechev and Dr. Michael Pradel, ETH Zürich): Spring 2013
  • Software Architecture and Engineering (Prof. Dr. Peter Müller, ETH Zürich): Spring 2012
  • Research Topics in Software Engineering (Prof. Dr. Peter Müller and Prof. Dr. Martin Vechev, ETH Zürich): Spring 2012 (head assistant)
  • Software and Security Testing (Prof. Dr. David Basin and Prof. Dr. Peter Müller, ETH Zürich): Fall 2011
  • Software Engineering (Prof. Dr. Peter Müller, ETH Zürich): Spring 2011 (head assistant), Spring 2010
  • Informatics II (Prof. Dr. Friedemann Mattern, ETH Zürich): Spring 2007
  • Informatics (Prof. Dr. Hans Hinterberger, ETH Zürich): Fall 2006

Supervised Students

  • Kostas Ferles (UT Austin, Ph.D. project, 2015–2016)
  • Ahmet Çelik (UT Austin, Ph.D. project, 2015–2016)
  • Roger Koradi (Bachelor's thesis, Spring 2015, co-supervised with Malte Schwerhoff, ETH Zürich)
  • David Rohr (Research project, Fall 2014, co-supervised with Maria Christakis, ETH Zürich)
  • Florian Egli (Master's thesis, Spring 2012, ETH Zürich)
  • Malte Schwerhoff (Research project, Fall 2010, ETH Zürich)

Contact Information

Validate