/ Courant Institute / Computer Science

I am a Professor of Computer Science at the Courant Institute of New York University and a member of the Analysis of Computer Systems Group. See my curriculum vitae for further details.

I presently serve as Chair of the Computer Science Department.

News & Highlights

  • 2026-09-01 — Congratulations to my former PhD student and Courant Faculty fellow Elaine Li, who is starting as an Assistant Professor at Barnard College, Columbia University!
  • 2026-09-01 — Congratulations to my former PhD student Ekanshdeep Gupta, who is joining NVIDIA's Rigorous Software Engineering and Validation team!
  • 2026-04-03 — Our paper "Implementability of Global Distributed Protocols modulo Network Architectures" (with Elaine Li) was accepted at PLDI 2026.

Research

My research focuses on program analysis and verification, automated deduction, and concurrency.

Current Research Projects

Raven

Raven is a deductive verifier for concurrent programs, built on a form of concurrent separation logic with SMT-backed proof automation. It aims to make full functional-correctness verification of fine-grained concurrent code practical, reducing much of the manual proof burden typically required by separation-logic-based reasoning.

Key Papers
  • Raven: An SMT-Based Concurrency Verifierpdf
    E. Gupta, N. Patel, and T. Wies
    In Computer Aided Verification (CAV), 2025
  • An Extension API for the Concurrent Program Verifier Raven
    E. Gupta and T. Wies
    In Formal Methods in Computer-Aided Design (FMCAD), 2026

Consistent Microservice Updates

This project studies how to safely evolve microservice-based distributed systems while they are running, so that rolling out an update never leaves the system in a state whose inconsistency is visible to clients. Our POPL'26 paper, joint with Devora Chait-Roth and Kedar Namjoshi, develops techniques for reasoning about and enforcing consistency during such updates at scale.

Key Papers

Global Protocol Implementability

Joint work with Elaine Li, together with Felix Stutz and Damien Zufferey, on when a global, choreographic specification of a multiparty distributed protocol can be faithfully realized by a collection of independently communicating processes. This line of work extends classical multiparty session type theory to protocols with richer, potentially infinite state, and develops both automated (SMT- and automata-based) and mechanically certified verification techniques for establishing implementability.

Key Papers

Selected Publications

Complete list of publications →

Teaching

Professional Activities

Organizer

Publications

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

Books

  1. Automated Verification of Concurrent Search Structurespdf
    S. Krishna, N. Patel, D. Shasha, and T. Wies
    Morgan & Claypool Publishers, 2021

In Journals

  1. Implementability of Global Distributed Protocols modulo Network Architecturesdoi
    E. Li and T. Wies
    PACMPL, 10(Programming Language Design and Implementation (PLDI)), 2026
  2. Consistent Updates for Scalable Microservicespdf
    D. Chait-Roth, K.S. Namjoshi, and T. Wies
    PACMPL, 10(Principles of Programming Languages (POPL)), 2026
  3. Abstract Interpretation of Temporal Safety Effects of Higher Order Programspdf
    M. Nicola, C. Agarwal, E. Koskinen, and T. Wies
    PACMPL, 9(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2025
  4. Characterizing Implementability of Global Protocols with Infinite States and Datapdf
    E. Li, F. Stutz, T. Wies, and D. Zufferey
    PACMPL, 9(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2025
  5. Embedding Hindsight Reasoning in Separation Logicpdf
    R. Meyer, T. Wies, and S. Wolff
    PACMPL, 7(Programming Language Design and Implementation (PLDI)), 2023
  6. A Concurrent Program Logic with a Future and Historypdf
    R. Meyer, T. Wies, and S. Wolff
    PACMPL, 6(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2022
  7. Verifying Concurrent Multicopy Search Structurespdf
    N. Patel, S. Krishna, D. Shasha, and T. Wies
    PACMPL, 5(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2021
  8. Dataflow Refinement Type Inferencepdftalk
    Z. Pavlinovic, Y. Su, and T. Wies
    PACMPL, 5(ACM Symposium on the Principles of Programming Languages (POPL)), 2021
  9. Go with the Flow: Compositional Abstractions for Concurrent Data Structurespdf
    S. Krishna, D. Shasha, and T. Wies
    PACMPL, 2(ACM Symposium on the Principles of Programming Languages (POPL)), 2018
  10. Complete Instantiation-Based Interpolationpdfdoi
    N. Totla and T. Wies
    Journal of Automated Reasoning, 57(1), 2016
  11. Preface - Invariant Generationpdfdoi
    G. Grov and T. Wies
    Science of Computer Programming (SCICO), 93, 2014
  12. Doomed Program Pointspdf
    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 Conferences

  1. An Extension API for the Concurrent Program Verifier Raven
    E. Gupta and T. Wies
    In Formal Methods in Computer-Aided Design (FMCAD), 2026
  2. Domain Faithfulness through Counterfactually Robust Learningpdf
    A. Balashankar, A. Bhardwaj, N. Madan, T. Wies, and L. Subramanian
    In Fifth Conference on Causal Learning and Reasoning, 2026
  3. The Privacy Quagmire: Bridging Computer Science and Legal Nuancepdf
    Y. Zhao, V. Chandrasekaran, T. Wies, and L. Subramanian
    In ACM Workshop on Hot Topics in Networks (HOTNETS), 2025
  4. Certified Implementability of Global Multiparty Protocolspdf
    E. Li and T. Wies
    In Interactive Theorem Proving (ITP), 2025
  5. Raven: An SMT-Based Concurrency Verifierpdf
    E. Gupta, N. Patel, and T. Wies
    In Computer Aided Verification (CAV), 2025
  6. Sprout: A Verifier for Symbolic Multiparty Protocolspdf
    E. Li, F. Stutz, T. Wies, and D. Zufferey
    In Computer Aided Verification (CAV), 2025
  7. Arithmetizing Shape Analysispdf
    S. Wolff, E. Gupta, Z. Esen, H. Hojjat, P. Rümmer, and T. Wies
    In Computer Aided Verification (CAV), 2025
  8. Verifying Lock-free Search Structure Templatespdf
    N. Patel, D. Shasha, and T. Wies
    In European Conference on Object-Oriented Programming (ECOOP), 2024
  9. Deciding Subtyping for Asynchronous Multiparty Sessionspdf
    E. Li, F. Stutz, and T. Wies
    In European Symposium on Programming (ESOP), 2024
  10. Complete Multiparty Session Type Projection with Automatapdf
    E. Li, F. Stutz, T. Wies, and D. Zufferey
    In Computer Aided Verification (CAV), 2023
  11. nekton: a linearizability proof checkerpdf
    R. Meyer, A. Opaterny, T. Wies, and S. Wolff
    In Computer Aided Verification (CAV), 2023
  12. Less is more: refinement proofs for probabilistic proofspdf
    K. Jiang, D. Chait-Roth, Z. DeStefano, M. Walfish, and T. Wies
    In IEEE Symposium on Security and Privacy (IEEE S&P), 2023
  13. Make flows small again: revisiting the flow frameworkpdf
    R. Meyer, T. Wies, and S. Wolff
    In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2023
  14. Needles in a Haystack: Using PORT to Catch Bad Behaviors within Application Recordingspdf
    P. Moore, T. Wies, M. Waldman, P. Frankl, and J. Cappos
    In International Conference on Software Technologies (ICSOFT), 2022
  15. Inverse-Weighted Survival Gamespdf
    M. Goldstein, X. Han, A.M. Puli, T. Wies, A.J. Perotte, and R. Ranganath
    In Conference on Neural Information Processing Systems (NeurIPS), 2021
  16. TarTar: A Timed Automata Repair Toolpdf
    M. Kölbl, S. Leue, and T. Wies
    In Computer Aided Verification (CAV), 2020
  17. Verifying Concurrent Search Structure Templatespdftalk
    S. Krishna, N. Patel, D. Shasha, and T. Wies
    In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2020
  18. Local Reasoning for Global Graph Propertiespdftalk
    S. Krishna, A.J. Summers, and T. Wies
    In European Symposium on Programming (ESOP), 2020
  19. Charting a Course Through Uncertain Environments: SEA Uses Past Problems to Avoid Future FailurespdfBest Paper Award
    P. Moore, J. Cappos, P. Frankl, and T. Wies
    In International Symposium on Software Reliability Engineering (ISSRE), 2019
  20. Clock Bound Repair for Timed Systemspdf
    M. Kölbl, S. Leue, and T. Wies
    In Computer Aided Verification (CAV), 2019
  21. VACCINE: Using Contextual Integrity for Data Leakage Detectionpdf
    Y. Shvartzshnaider, Z. Pavlinovic, A. Balashankar, T. Wies, L. Subramanian, H. Nissenbaum, and P. Mittal
    In World Wide Web Conference (WWW), 2019
  22. Full accounting for verifiable outsourcingpdf
    R. Wahby, Y. Ji, A.J. Blumberg, a. shelat, J. Thaler, M. Walfish, and T. Wies
    In ACM Conference on Computer and Communications Security (CCS), 2017
  23. Partitioned Memory Models for Program Analysispdf
    W. Wang, C. Barrett, and T. Wies
    In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2017
  24. Error Invariants for Concurrent Tracespdf
    A. Holzer, D. Schwartz-Narbonne, M. Tabaei, G. Weissenbacher, and T. Wies
    In International Symposium on Formal Methods (FM), 2016
  25. Learning Privacy Expectations by Crowdsourcing Contextual Informational Normspdf
    Y. Shvartzshnaider, S. Tong, T. Wies, P. Kift, H. Nissenbaum, L. Subramanian, and P. Mittal
    In AAAI Conference on Human Computation and Crowdsourcing (HCOMP), 2016
  26. Classifying Bugs with Interpolantspdf
    A. Podelski, M. Schäf, and T. Wies
    In Tests and Proofs (TAP), 2016
  27. Practical SMT-Based Type Error Localizationpdf
    Z. Pavlinovic, T. King, and T. Wies
    In ACM SIGPLAN International Conference on Functional Programming (ICFP), 2015
  28. Deciding Local Theory Extensions via E-Matchingpdf
    K. Bansal, T. King, A. Reynolds, C. Barrett, and T. Wies
    In Computer Aided Verification (CAV), 2015
  29. VERMEER: A Tool for Tracing and Explaining Faulty C Programspdf
    D. Schwartz-Narbonne, C. Oh, M. Schäf, and T. Wies
    In International Conference on Software Engineering (ICSE), Demonstrations Track, 2015
  30. Conflict-Directed Graph Coveragepdf
    D. Schwartz-Narbonne, M. Schäf, D. Jovanović, P. Rümmer, and T. Wies
    In NASA Formal Methods (NFM), 2015
  31. Finding Minimum Type Error SourcespdfBest Paper Award
    Z. Pavlinovic, T. King, and T. Wies
    In ACM SIGPLAN International Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA), 2014
  32. Concolic Fault Abstractionpdf
    C. Oh, M. Schäf, D. Schwartz-Narbonne, and T. Wies
    In IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM), 2014
  33. Automating Separation Logic with Trees and Datapdf
    R. Piskac, T. Wies, and D. Zufferey
    In Computer Aided Verification (CAV), 2014
  34. Dynamic Package Interfacespdf
    S. Esmaeilsabzali, R. Majumdar, T. Wies, and D. Zufferey
    In Fundamental Approaches to Software Engineering (FASE), 2014
  35. GRASShopper: Complete Heap Verification with Mixed Specificationspdf
    R. Piskac, T. Wies, and D. Zufferey
    In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014
  36. Cascade 2.0pdf
    W. Wang, C. Barrett, and T. Wies
    In VMCAI, 2014
  37. Explaining Inconsistent Codepdf
    M. Schäf, T. Wies, and D. Schwartz-Narbonne
    In ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 2013
  38. Automating Separation Logic using SMTpdf
    R. Piskac, T. Wies, and D. Zufferey
    In Computer Aided Verification (CAV), 2013
  39. Structural Counter Abstractionpdf
    K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
    In TACAS, 2013
  40. Flow-Sensitive Fault Localizationpdf
    J. Christ, E. Ermis, M. Schäf, and T. Wies
    In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013
  41. Complete Instantiation-Based Interpolationpdf
    N. Totla and T. Wies
    In ACM Symposium on the Principles of Programming Languages (POPL), 2013
  42. Error Invariantspdf
    E. Ermis, M. Schäf, and T. Wies
    In Formal Methods (FM), 2012
  43. Deciding Functional Lists with Sublist Setspdf
    T. Wies, M. Muñiz, and V. Kuncak
    In Verified Software: Theories, Tools, Experiments (VSTTE), 2012
  44. Ideal Abstractions for Well-Structured Transition Systemspdf
    D. Zufferey, T. Wies, and T.A. Henzinger
    In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2012
  45. An Efficient Decision Procedure for Imperative Tree Data Structurespdf
    T. Wies, M. Muñiz, and V. Kuncak
    In Conference on Automated Deduction (CADE-23), 2011
  46. Scheduling Large Jobs by Abstraction Refinementpdf
    T.A. Henzinger, V. Singh, T. Wies, and D. Zufferey
    In European Conference on Computer Systems (EuroSys), 2011
  47. Decision Procedures for Automating Termination Proofspdf
    R. Piskac and T. Wies
    In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011
  48. A Marketplace for Cloud Computingpdf
    T.A. Henzinger, V. Singh, A. Tomar, T. Wies, and D. Zufferey
    In International Conference on Embedded Systems (EMSOFT), 2010
  49. FlexPRICE: Flexible Provisioning of Resources in a Cloud Environmentpdf
    T.A. Henzinger, V. Singh, A. Tomar, T. Wies, and D. Zufferey
    In IEEE International Conference on Cloud Computing (IEEE CLOUD), 2010
  50. Forward Analysis of Depth-Bounded Processespdf
    T. Wies, D. Zufferey, and T.A. Henzinger
    In Foundations of Software Science and Computation Structures (FoSSaCS), 2010
  51. Counterexample-guided focuspdfslides
    A. Podelski and T. Wies
    In ACM Symposium on the Principles of Programming Languages (POPL), 2010
  52. Building a Calculus of Data Structurespdf
    V. Kuncak, R. Piskac, P. Suter, and T. Wies
    In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2010
  53. Combining Theories with Shared Set Operationspdfslides
    T. Wies, R. Piskac, and V. Kuncak
    In Symposium on Frontiers of Combining Systems (FroCoS), 2009
  54. Abstraction Refinement for Quantified Array Assertionspdf
    M.N. Seghir, A. Podelski, and T. Wies
    In Static Analysis Symposium (SAS), 2009
  55. It's Doomed; We Can Prove Itpdf
    J. Hoenicke, K.R.M. Leino, A. Podelski, M. Schäf, and T. Wies
    In Formal Methods (FM), 2009
  56. Intra-module Inferencepdf
    S.K. Lahiri, S. Qadeer, J.P. Galeotti, J.W. Voung, and T. Wies
    In Computer Aided Verification (CAV), 2009
  57. Heap Assumptions on Demandpdf
    A. Podelski, A. Rybalchenko, and T. Wies
    In Computer Aided Verification (CAV), 2008
  58. Shape Analysis for Composite Data Structurespdf
    J. Berdine, C. Calcagno, B. Cook, D. Distefano, P.W. O'Hearn, T. Wies, and H. Yang
    In Computer Aided Verification (CAV), 2007
  59. Using First-Order Theorem Provers in the Jahob Data Structure Verification Systempdf
    C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M.C. Rinard
    In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2007
  60. Field Constraint Analysispdf
    T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard
    In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2006
  61. Boolean Heapspdf
    A. Podelski and T. Wies
    In Static Analysis Symposium (SAS), 2005

In Workshops

  1. RECIPE: Applying Open Domain Question Answering to Privacy Policiespdf
    Y. Shvartzshanider, A. Balashankar, T. Wies, and L. Subramanian
    In Workshop on Machine Reading for Question Answering@ACL, 2018
  2. Static Scheduling in Cloudspdf
    T.A. Henzinger, A.V. Singh, V. Singh, T. Wies, and D. Zufferey
    In USENIX Workshop on Hot Topics in Cloud Computing (HotCloud), 2011
  3. (EC)^2 in EC2pdf
    T.A. Henzinger, A.V. Singh, V. Singh, T. Wies, and D. Zufferey
    In Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2), 2011
  4. Verifying Complex Properties using Symbolic Shape Analysispdf
    T. Wies, V. Kuncak, K. Zee, A. Podelski, and M. Rinard
    In Workshop on Heap Analysis and Verification (HAV), 2007

Thesis

  1. Symbolic Shape Analysispdf
    T. Wies
    University of Freiburg, Freiburg, Germany, 2009

Technical Reports

  1. Consistent Updates for Scalable Microservices
    D. Chait-Roth, K.S. Namjoshi, and T. Wies
    arXiv Technical Report, abs/2508.04829, 2025
  2. Complete Multiparty Session Type Projection with Automatapdfdoi
    E. Li, F. Stutz, T. Wies, and D. Zufferey
    arXiv Technical Report, abs/2305.17079, 2023
  3. Less is more: refinement proofs for probabilistic proofspdf
    K. Jiang, D. Chait-Roth, Z. DeStefano, M. Walfish, and T. Wies
    IACR Cryptol. ePrint Arch. Technical Report, 2022/1557, 2022
  4. Embedding Hindsight Reasoning in Separation Logicpdfdoi
    R. Meyer, T. Wies, and S. Wolff
    arXiv Technical Report, abs/2209.13692, 2022
  5. A Concurrent Program Logic with a Future and Historypdfdoi
    R. Meyer, T. Wies, and S. Wolff
    arXiv Technical Report, arXiv:2207.02355, 2022
  6. Local Reasoning for Global Graph Propertiespdf
    S. Krishna, A.J. Summers, and T. Wies
    arXiv Technical Report, arXiv:1911.08632, 2019
  7. Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version)pdf
    S. Krishna, D. Shasha, and T. Wies
    arXiv Technical Report, arXiv:1711.03272, 2017
  8. On Structural Counter Abstractionpdf
    K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
    NYU Technical Report, TR2012-947, 2013
  9. Automating Separation Logic Using SMTpdf
    R. Piskac, T. Wies, and D. Zufferey
    NYU Technical Report, TR2013-954, 2013
  10. Complete Instantiation-Based Interpolationpdf
    N. Totla and T. Wies
    NYU Technical Report, TR2012-950, 2012
  11. On An Efficient Decision Procedure for Imperative Tree Data Structurespdf
    T. Wies, M. Muñiz, and V. Kuncak
    IST Technical Report, IST-2011-0005, 2011
  12. On Deciding Functional Lists with Sublist Setspdf
    T. Wies, M. Mu\~n, and V. Kuncak
    EPFL Technical Report, EPFL-REPORT-148361, 2010
  13. On Combining Theories with Shared Set Operationspdf
    T. Wies, R. Piskac, and V. Kuncak
    EPFL Technical Report, LARA-REPORT-2009-002, 2009
  14. On Set-Driven Combination of Logics and Verifierspdf
    T. Wies and V. Kuncak
    EPFL Technical Report, LARA-REPORT-2009-001, 2009
  15. On Field Constraint Analysispdf
    T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard
    MIT CSAIL Technical Report, MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010, 2005