Profile picture

Contact

lastname@cs.nyu.edu
+1 (212) 998 3293
Room 407
Warren Weaver Hall
251 Mercer St
New York, NY 10012

Group Members

Postdoc

Daniel Schwartz-Narbonne

PhD Students

Chanseok Oh
Siddharth Krishna
Zvonimir Pavlinovic
Kshitij Bansal (co-advisor)
Wei Wang (co-advisor)

Research

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

Recent Publications

  • Practical SMT-Based Type Error Localization

    Z. Pavlinovic, T. King, and T. Wies
    To appear in Proceedings of ACM SIGPLAN International Conference on Functional Programming (ICFP), 2015
  • Deciding Local Theory Extensions via E-Matching

    K. Bansal, T. King, A. Reynolds, C. Barrett, and T. Wies
    To appear in Proceedings of Computer Aided Verification (CAV), 2015
  • VERMEER: A Tool for Tracing and Explaining Faulty C Programs pdf

    D. Schwartz-Narbonne, C. Oh, M. Schäf, and T. Wies
    To appear in Proceedings of International Conference on Software Engineering (ICSE), Demonstrations Track, 2015
  • Context-Directed Graph Coverage pdf

    D. Schwartz-Narbonne, M. Schäf, D. Jovanović, P. Rümmer, and T. Wies
    In Proceedings of NASA Formal Methods (NFM), 2015
  • Finding Minimum Type Error Sources pdf Best Paper Award

    Z. Pavlinovic, T. King, and T. Wies
    In Proceedings of ACM SIGPLAN International Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA), 2014
  • Automating Separation Logic with Trees and Data pdf

    R. Piskac, T. Wies, and D. Zufferey
    In Proceedings of Computer Aided Verification (CAV), 2014

Complete list of publications

Recent Invited Talks

Tools

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

  • GRASShopper

    A verification tool that checks functional correctness of programs manipulating heap-allocated data structures.
  • Vermeer

    An automated debugging tool that traces and explains faults in C programs.
  • Picasso

    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

    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

    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

    A tool for automatic formal verification of industrial low-level software components. SLAyer is being developed at Microsoft Research Cambridge.
  • HAVOC

    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.

Teaching

Professional Activities

Publications

See also my DBLP entry for a complete list of my publications.

In Conferences

  1. Practical SMT-Based Type Error Localization

    Z. Pavlinovic, T. King, and T. Wies
    To appear in Proceedings of ACM SIGPLAN International Conference on Functional Programming (ICFP), 2015
  2. Deciding Local Theory Extensions via E-Matching

    K. Bansal, T. King, A. Reynolds, C. Barrett, and T. Wies
    To appear in Proceedings of Computer Aided Verification (CAV), 2015
  3. VERMEER: A Tool for Tracing and Explaining Faulty C Programs pdf

    D. Schwartz-Narbonne, C. Oh, M. Schäf, and T. Wies
    To appear in Proceedings of International Conference on Software Engineering (ICSE), Demonstrations Track, 2015
  4. Context-Directed Graph Coverage pdf

    D. Schwartz-Narbonne, M. Schäf, D. Jovanović, P. Rümmer, and T. Wies
    In Proceedings of NASA Formal Methods (NFM), 2015
  5. Finding Minimum Type Error Sources pdf Best Paper Award

    Z. Pavlinovic, T. King, and T. Wies
    In Proceedings of ACM SIGPLAN International Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA), 2014
  6. Concolic Fault Abstraction pdf

    C. Oh, M. Schäf, D. Schwartz-Narbonne, and T. Wies
    In Proceedings of IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM), 2014
  7. Automating Separation Logic with Trees and Data pdf

    R. Piskac, T. Wies, and D. Zufferey
    In Proceedings of Computer Aided Verification (CAV), 2014
  8. Dynamic Package Interfaces pdf

    S. Esmaeilsabzali, R. Majumdar, T. Wies, and D. Zufferey
    In Proceedings of Fundamental Approaches to Software Engineering (FASE), 2014
  9. GRASShopper: Complete Heap Verification with Mixed Specifications pdf

    R. Piskac, T. Wies, and D. Zufferey
    In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014
  10. Cascade 2.0 pdf

    W. Wang, C. Barrett, and T. Wies
    In Proceedings of VMCAI, 2014
  11. Explaining Inconsistent Code pdf

    M. Schäf, T. Wies, and D. Schwartz-Narbonne
    In Proceedings of ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 2013
  12. Automating Separation Logic using SMT pdf

    R. Piskac, T. Wies, and D. Zufferey
    In Proceedings of Computer Aided Verification (CAV), 2013
  13. Structural Counter Abstraction pdf

    K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
    In Proceedings of TACAS, 2013
  14. Flow-Sensitive Fault Localization pdf

    J. Christ, E. Ermis, M. Schäf, and T. Wies
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013
  15. Complete Instantiation-Based Interpolation pdf

    N. Totla and T. Wies
    In Proceedings of ACM Symposium on the Principles of Programming Languages (POPL), 2013
  16. Error Invariants pdf

    E. Ermis, M. Schäf, and T. Wies
    In Proceedings of Formal Methods (FM), 2012
  17. Deciding Functional Lists with Sublist Sets pdf

    T. Wies, M. Muñiz, and V. Kuncak
    In Proceedings of Verified Software: Theories, Tools, Experiments (VSTTE), 2012
  18. Ideal Abstractions for Well-Structured Transition Systems pdf

    D. Zufferey, T. Wies, and T.A. Henzinger
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2012
  19. An Efficient Decision Procedure for Imperative Tree Data Structures pdf

    T. Wies, M. Muñiz, and V. Kuncak
    In Proceedings of Conference on Automated Deduction (CADE-23), 2011
  20. Scheduling Large Jobs by Abstraction Refinement pdf

    T.A. Henzinger, V. Singh, T. Wies, and D. Zufferey
    In Proceedings of European Conference on Computer Systems (EuroSys), 2011
  21. Decision Procedures for Automating Termination Proofs pdf

    R. Piskac and T. Wies
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011
  22. A Marketplace for Cloud Computing pdf

    T.A. Henzinger, V. Singh, A. Tomar, T. Wies, and D. Zufferey
    In Proceedings of International Conference on Embedded Systems (EMSOFT), 2010
  23. FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment pdf

    T.A. Henzinger, V. Singh, A. Tomar, T. Wies, and D. Zufferey
    In Proceedings of IEEE International Conference on Cloud Computing (IEEE CLOUD), 2010
  24. Forward Analysis of Depth-Bounded Processes pdf

    T. Wies, D. Zufferey, and T.A. Henzinger
    In Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS), 2010
  25. Counterexample-guided focus pdf slides

    A. Podelski and T. Wies
    In Proceedings of ACM Symposium on the Principles of Programming Languages (POPL), 2010
  26. Building a Calculus of Data Structures pdf

    V. Kuncak, R. Piskac, P. Suter, and T. Wies
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2010
  27. Combining Theories with Shared Set Operations pdf slides

    T. Wies, R. Piskac, and V. Kuncak
    In Proceedings of Symposium on Frontiers of Combining Systems (FroCoS), 2009
  28. It's Doomed; We Can Prove It pdf

    J. Hoenicke, K.R.M. Leino, A. Podelski, M. Schäf, and T. Wies
    In Proceedings of Formal Methods (FM), 2009
  29. Abstraction Refinement for Quantified Array Assertions pdf

    M.N. Seghir, A. Podelski, and T. Wies
    In Proceedings of Static Analysis Symposium (SAS), 2009
  30. Intra-module Inference pdf

    S.K. Lahiri, S. Qadeer, J.P. Galeotti, J.W. Voung, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2009
  31. Heap Assumptions on Demand pdf

    A. Podelski, A. Rybalchenko, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2008
  32. Shape Analysis for Composite Data Structures pdf

    J. Berdine, C. Calcagno, B. Cook, D. Distefano, P.W. O'Hearn, T. Wies, and H. Yang
    In Proceedings of Computer Aided Verification (CAV), 2007
  33. Using First-Order Theorem Provers in the Jahob Data Structure Verification System pdf

    C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M.C. Rinard
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2007
  34. Field Constraint Analysis pdf

    T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2006
  35. Boolean Heaps pdf

    A. Podelski and T. Wies
    In Proceedings of Static Analysis Symposium (SAS), 2005

In Journals

  1. Preface - Invariant Generation pdf

    G. Grov and T. Wies
    Science of Computer Programming (SCICO), 93, 2014
  2. Doomed Program Points pdf

    J. Hoenicke, K.R.M. Leino, A. Podelski, M. Schäf, and T. Wies
    Formal Methods in System Design (FMSD), 37(2-3), 2010

In Workshops

  1. Static Scheduling in Clouds pdf

    T.A. Henzinger, A.V. Singh, V. Singh, T. Wies, and D. Zufferey
    In Proceedings of USENIX Workshop on Hot Topics in Cloud Computing (HotCloud), 2011
  2. (EC)^2 in EC2 pdf

    T.A. Henzinger, A.V. Singh, V. Singh, T. Wies, and D. Zufferey
    In Proceedings of Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2), 2011
  3. Verifying Complex Properties using Symbolic Shape Analysis pdf

    T. Wies, V. Kuncak, K. Zee, A. Podelski, and M. Rinard
    In Proceedings of Workshop on Heap Analysis and Verification (HAV), 2007

Thesis

  1. Symbolic Shape Analysis pdf

    T. Wies
    University of Freiburg, Freiburg, Germany, 2009

Technical Reports

  1. On Structural Counter Abstraction pdf

    K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
    NYU Technical Report, TR2012-9472013
  2. Automating Separation Logic Using SMT pdf

    R. Piskac, T. Wies, and D. Zufferey
    NYU Technical Report, TR2013-9542013
  3. Complete Instantiation-Based Interpolation pdf

    N. Totla and T. Wies
    NYU Technical Report, TR2012-9502012
  4. On An Efficient Decision Procedure for Imperative Tree Data Structures pdf

    T. Wies, M. Muñiz, and V. Kuncak
    IST Technical Report, IST-2011-00052011
  5. On Deciding Functional Lists with Sublist Sets pdf

    T. Wies, M. Mu\~n, and V. Kuncak
    EPFL Technical Report, EPFL-REPORT-1483612010
  6. On Combining Theories with Shared Set Operations pdf

    T. Wies, R. Piskac, and V. Kuncak
    EPFL Technical Report, LARA-REPORT-2009-0022009
  7. On Set-Driven Combination of Logics and Verifiers pdf

    T. Wies and V. Kuncak
    EPFL Technical Report, LARA-REPORT-2009-0012009
  8. On Field Constraint Analysis pdf

    T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard
    MIT CSAIL Technical Report, MIT-CSAIL-TR-2005-072, MIT-LCS-TR-10102005