Thomas Wies

Computer Science Department
Courant Institute of Mathematical Sciences
New York University

I am an Assistant Professor in the NYU Computer Science Department and a member of the Analysis of Computer Systems Group in the Courant Institute. I received my doctorate in Computer Science from the University of Freiburg, Germany (2009). Before joining NYU, I held post-doctoral positions at École Polytechnique Fédérale de Lausanne, Switzerland and at the Institute of Science and Technology Austria.

See also my curriculum vitae.


My research focuses on program analysis and verification, automated deduction, concurrent software, and software productivity.

Recent Publications

Complete list of publications

Recent Invited Talks


As a byproduct of my research projects, I have developed and contributed to a number of tools.

  • GRASShopper is a verification tool that checks functional correctness of programs manipulating heap-allocated data structures.
  • Vermeer is an automated debugging tool that traces and explains faults in C programs.
  • Picasso is a static analyzer for depth-bounded concurrent systems. It has been used to verify properties of non-blocking concurrent data structures and distributed message passing algorithms with an unbounded number of threads and messages.
  • Jahob is a verification system for programs written in a subset of Java. Using Jahob, developers can statically prove that methods satisfy their contracts in all possible executions, as well as that they preserve essential structural invariants and design constraints.
  • Bohne is a symbolic shape analysis tool. It infers loop invariants of programs manipulating heap-allocated data structures. Bohne is integrated into the Jahob verification system.
  • SLAyer is a tool for automatic formal verification of industrial low-level software components. SLAyer is being developed at Microsoft Research Cambridge.
  • HAVOC is a tool for specifying and checking properties of systems software written in C, in the presence of pointer manipulations, unsafe casts and dynamic memory allocation.
  • HAVOC is being developed at Microsoft Research Redmond.


Professional Activities

Program committee member: