Contact
| wies at cs.nyu.edu |
| +1 (212) 998 3293 |
| 60 Fifth Avenue
Room 403 New York, NY 10011 |
Group Members
Faculty Fellows |
| Elaine Li |
Ph.D. Students |
| Devora Chait-Roth |
| Ekanshdeep Gupta |
| Jacob Salzberg (co-advisor) |
Group Alumni |
| Kshitij Bansal (co-advisor) |
| Siddharth Krishna |
| Chanseok Oh |
| Zvonimir Pavlinovic |
| Nisarg Patel |
| Daniel Schwartz-Narbonne |
| Yan Shvartzshnaider |
| Wei Wang (co-advisor) |
| Sebastian Wolff |
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.
Research
My research focuses on program analysis and verification, automated deduction, and concurrency.
Selected Publications
-
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs pdf
M. Nicola, C. Agarwal, E. Koskinen, and T. Wies
PACMPL, 9(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2025 -
Characterizing Implementability of Global Protocols with Infinite States and Data pdf
E. Li, F. Stutz, T. Wies, and D. Zufferey
PACMPL, 9(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2025 -
Certified Implementability of Global Multiparty Protocols pdf
E. Li and T. Wies
In Proceedings of Interactive Theorem Proving (ITP), 2025 -
Raven: An SMT-Based Concurrency Verifier pdf
E. Gupta, N. Patel, and T. Wies
In Proceedings of Computer Aided Verification (CAV), 2025 -
Sprout: A Verifier for Symbolic Multiparty Protocols pdf
E. Li, F. Stutz, T. Wies, and D. Zufferey
In Proceedings of Computer Aided Verification (CAV), 2025 -
Arithmetizing Shape Analysis pdf
S. Wolff, E. Gupta, Z. Esen, H. Hojjat, P. Rümmer, and T. Wies
In Proceedings of Computer Aided Verification (CAV), 2025 -
Verifying Lock-free Search Structure Templates pdf
N. Patel, D. Shasha, and T. Wies
In Proceedings of European Conference on Object-Oriented Programming (ECOOP), 2024 -
Less is more: refinement proofs for probabilistic proofs pdf
K. Jiang, D. Chait-Roth, Z. DeStefano, M. Walfish, and T. Wies
In Proceedings of IEEE Symposium on Security and Privacy (IEEE S&P), 2023 -
Embedding Hindsight Reasoning in Separation Logic pdf
R. Meyer, T. Wies, and S. Wolff
PACMPL, 7(Programming Language Design and Implementation (PLDI)), 2023 -
Make flows small again: revisiting the flow framework pdf
R. Meyer, T. Wies, and S. Wolff
In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2023 -
A Concurrent Program Logic with a Future and History pdf
R. Meyer, T. Wies, and S. Wolff
PACMPL, 6(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2022 -
Inverse-Weighted Survival Games pdf
M. Goldstein, X. Han, A.M. Puli, T. Wies, A.J. Perotte, and R. Ranganath
In Proceedings of Conference on Neural Information Processing Systems (NeurIPS), 2021 -
Automated Verification of Concurrent Search Structures pdf
S. Krishna, N. Patel, D. Shasha, and T. Wies
Morgan & Claypool Publishers, 2021 -
Automating Separation Logic using SMT pdf
R. Piskac, T. Wies, and D. Zufferey
In Proceedings of Computer Aided Verification (CAV), 2013
Selected Invited Talks and Lectures
- International Conference on Concurrency Theory, Calgary, Canada, September 2024
- Eleventh Summer School on Formal Techniques, Menlo Park, CA, USA, June 2022
- Simons Institute Seminar on "Theoretical Foundations of Computer Systems", February 2021
- Effective Verification: Static Analysis Meets Program Logics, Leiden, Netherlands, May 2019.
- 16th International Workshop on Satisfiability Modulo Theories, Oxford, UK, July 2018.
- Summer School on Verification Technology, Systems, & Applications, Saarbrücken, Germany, July-August 2017.
- International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning, Lisbon, Portugal, June 2016.
- International Conference on Verification, Model Checking, and Abstract Interpretation, San Diego, CA, USA, January 2014.
Tools
As a byproduct of my research, I have developed and contributed to a number of tools.
-
Raven
A deductive verifier for concurrent programs based on concurrent separation logic. -
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.
Teaching
-
Principles of Programming Languages (undergraduate)
-
Programming Languages (graduate)
-
Computer Systems Organization (undergraduate)
-
Object-Oriented Programming (graduate)
Object-Oriented Programming (undergraduate)
-
Rigorous Software Development (graduate)
-
Programming Paradigms for Concurrency (graduate)
Professional Activities
Organizer
- Co-organizer of VerifyThis 2025
- Program co-chair of NETYS 2023
- Program chair of ESOP 2023
- Program co-chair of VMCAI 2022
- Fellowship chair of CAV 2021
- Fellowship chair of CAV 2020
- Program co-chair of SYNT 2019
- Fellowship chair of CAV 2019
- Program co-chair of VSTTE 2017
- Program chair of TAPAS 2017
- Program co-chair of WING 2012
Program Committee Member
- VMCAI 2026
- POPL 2024, FMCAD 2024
- IEEE S&P 2023
- PLDI 2022
- FMCAD 2021, VSTTE 2021
- POPL 2020, VMCAI 2020, ADSL 2020, NETYS 2020, VSTTE 2020, VDS 2020 (co-chair)
- TACAS 2019, SYNT 2019 (co-chair)
- CAV 2018, TACAS 2018, VMCAI 2018, VSTTE 2018, ADSL 2018
- ECOOP 2017, TACAS 2017, TMPA 2017, VSTTE 2017 (co-chair), CREST 2017, CONCUR 2017, Onward! 2017, TAPAS 2017 (chair)
- POPL 2016 (ERC), VMCAI 2016, CAV 2016
- VMCAI 2015
- POPL 2014, SMT 2014, FOOL 2014
- VSTTE 2013
- WING 2012 (co-chair), BOOGIE 2012, FTfJP 2012, SAS 2012, VSTTE 2012
- WING 2010
- WING 2009
Publications
See also my DBLP entry for a complete list of my publications.
Books
-
Automated Verification of Concurrent Search Structures pdf
S. Krishna, N. Patel, D. Shasha, and T. Wies
Morgan & Claypool Publishers, 2021
In Journals
-
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs pdf
M. Nicola, C. Agarwal, E. Koskinen, and T. Wies
PACMPL, 9(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2025 -
Characterizing Implementability of Global Protocols with Infinite States and Data pdf
E. Li, F. Stutz, T. Wies, and D. Zufferey
PACMPL, 9(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2025 -
Embedding Hindsight Reasoning in Separation Logic pdf
R. Meyer, T. Wies, and S. Wolff
PACMPL, 7(Programming Language Design and Implementation (PLDI)), 2023 -
A Concurrent Program Logic with a Future and History pdf
R. Meyer, T. Wies, and S. Wolff
PACMPL, 6(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2022 -
Verifying Concurrent Multicopy Search Structures pdf
N. Patel, S. Krishna, D. Shasha, and T. Wies
PACMPL, 5(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2021 -
Dataflow Refinement Type Inference pdf talk
Z. Pavlinovic, Y. Su, and T. Wies
PACMPL, 5(ACM Symposium on the Principles of Programming Languages (POPL)), 2021 -
Go with the Flow: Compositional Abstractions for Concurrent Data Structures pdf
S. Krishna, D. Shasha, and T. Wies
PACMPL, 2(ACM Symposium on the Principles of Programming Languages (POPL)), 2018 -
Complete Instantiation-Based Interpolation pdf
N. Totla and T. Wies
Journal of Automated Reasoning, 57(1), 2016 -
Preface - Invariant Generation pdf
G. Grov and T. Wies
Science of Computer Programming (SCICO), 93, 2014 -
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 Conferences
-
Certified Implementability of Global Multiparty Protocols pdf
E. Li and T. Wies
In Proceedings of Interactive Theorem Proving (ITP), 2025 -
Raven: An SMT-Based Concurrency Verifier pdf
E. Gupta, N. Patel, and T. Wies
In Proceedings of Computer Aided Verification (CAV), 2025 -
Sprout: A Verifier for Symbolic Multiparty Protocols pdf
E. Li, F. Stutz, T. Wies, and D. Zufferey
In Proceedings of Computer Aided Verification (CAV), 2025 -
Arithmetizing Shape Analysis pdf
S. Wolff, E. Gupta, Z. Esen, H. Hojjat, P. Rümmer, and T. Wies
In Proceedings of Computer Aided Verification (CAV), 2025 -
Verifying Lock-free Search Structure Templates pdf
N. Patel, D. Shasha, and T. Wies
In Proceedings of European Conference on Object-Oriented Programming (ECOOP), 2024 -
Deciding Subtyping for Asynchronous Multiparty Sessions pdf
E. Li, F. Stutz, and T. Wies
In Proceedings of European Symposium on Programming (ESOP), 2024 -
Complete Multiparty Session Type Projection with Automata pdf
E. Li, F. Stutz, T. Wies, and D. Zufferey
In Proceedings of Computer Aided Verification (CAV), 2023 -
nekton: a linearizability proof checker pdf
R. Meyer, A. Opaterny, T. Wies, and S. Wolff
In Proceedings of Computer Aided Verification (CAV), 2023 -
Less is more: refinement proofs for probabilistic proofs pdf
K. Jiang, D. Chait-Roth, Z. DeStefano, M. Walfish, and T. Wies
In Proceedings of IEEE Symposium on Security and Privacy (IEEE S&P), 2023 -
Make flows small again: revisiting the flow framework pdf
R. Meyer, T. Wies, and S. Wolff
In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2023 -
Needles in a Haystack: Using PORT to Catch Bad Behaviors within Application Recordings pdf
P. Moore, T. Wies, M. Waldman, P. Frankl, and J. Cappos
In Proceedings of International Conference on Software Technologies (ICSOFT), 2022 -
Inverse-Weighted Survival Games pdf
M. Goldstein, X. Han, A.M. Puli, T. Wies, A.J. Perotte, and R. Ranganath
In Proceedings of Conference on Neural Information Processing Systems (NeurIPS), 2021 -
TarTar: A Timed Automata Repair Tool pdf
M. Kölbl, S. Leue, and T. Wies
In Proceedings of Computer Aided Verification (CAV), 2020 -
Verifying Concurrent Search Structure Templates pdf talk
S. Krishna, N. Patel, D. Shasha, and T. Wies
In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2020 -
Local Reasoning for Global Graph Properties pdf talk
S. Krishna, A.J. Summers, and T. Wies
In Proceedings of European Symposium on Programming (ESOP), 2020 -
Charting a Course Through Uncertain Environments: SEA Uses Past Problems to Avoid Future Failures pdf Best Paper Award
P. Moore, J. Cappos, P. Frankl, and T. Wies
In Proceedings of International Symposium on Software Reliability Engineering (ISSRE), 2019 -
Clock Bound Repair for Timed Systems pdf
M. Kölbl, S. Leue, and T. Wies
In Proceedings of Computer Aided Verification (CAV), 2019 -
VACCINE: Using Contextual Integrity for Data Leakage Detection pdf
Y. Shvartzshnaider, Z. Pavlinovic, A. Balashankar, T. Wies, L. Subramanian, H. Nissenbaum, and P. Mittal
In Proceedings of World Wide Web Conference (WWW), 2019 -
Full accounting for verifiable outsourcing pdf
R. Wahby, Y. Ji, A.J. Blumberg, a. shelat, J. Thaler, M. Walfish, and T. Wies
In Proceedings of ACM Conference on Computer and Communications Security (CCS), 2017 -
Partitioned Memory Models for Program Analysis pdf
W. Wang, C. Barrett, and T. Wies
In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2017 -
Error Invariants for Concurrent Traces pdf
A. Holzer, D. Schwartz-Narbonne, M. Tabaei, G. Weissenbacher, and T. Wies
In Proceedings of International Symposium on Formal Methods (FM), 2016 -
Learning Privacy Expectations by Crowdsourcing Contextual Informational Norms pdf
Y. Shvartzshnaider, S. Tong, T. Wies, P. Kift, H. Nissenbaum, L. Subramanian, and P. Mittal
In Proceedings of AAAI Conference on Human Computation and Crowdsourcing (HCOMP), 2016 -
Classifying Bugs with Interpolants pdf
A. Podelski, M. Schäf, and T. Wies
In Proceedings of Tests and Proofs (TAP), 2016 -
Practical SMT-Based Type Error Localization pdf
Z. Pavlinovic, T. King, and T. Wies
In Proceedings of ACM SIGPLAN International Conference on Functional Programming (ICFP), 2015 -
Deciding Local Theory Extensions via E-Matching pdf
K. Bansal, T. King, A. Reynolds, C. Barrett, and T. Wies
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
In Proceedings of International Conference on Software Engineering (ICSE), Demonstrations Track, 2015 -
Conflict-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 -
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 -
Automating Separation Logic with Trees and Data pdf
R. Piskac, T. Wies, and D. Zufferey
In Proceedings of Computer Aided Verification (CAV), 2014 -
Dynamic Package Interfaces pdf
S. Esmaeilsabzali, R. Majumdar, T. Wies, and D. Zufferey
In Proceedings of Fundamental Approaches to Software Engineering (FASE), 2014 -
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 -
Cascade 2.0 pdf
W. Wang, C. Barrett, and T. Wies
In Proceedings of VMCAI, 2014 -
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 -
Automating Separation Logic using SMT pdf
R. Piskac, T. Wies, and D. Zufferey
In Proceedings of Computer Aided Verification (CAV), 2013 -
Structural Counter Abstraction pdf
K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
In Proceedings of TACAS, 2013 -
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 -
Complete Instantiation-Based Interpolation pdf
N. Totla and T. Wies
In Proceedings of ACM Symposium on the Principles of Programming Languages (POPL), 2013 -
Error Invariants pdf
E. Ermis, M. Schäf, and T. Wies
In Proceedings of Formal Methods (FM), 2012 -
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 -
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 -
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 -
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 -
Decision Procedures for Automating Termination Proofs pdf
R. Piskac and T. Wies
In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011 -
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 -
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 -
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 -
Counterexample-guided focus pdf slides
A. Podelski and T. Wies
In Proceedings of ACM Symposium on the Principles of Programming Languages (POPL), 2010 -
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 -
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 -
Abstraction Refinement for Quantified Array Assertions pdf
M.N. Seghir, A. Podelski, and T. Wies
In Proceedings of Static Analysis Symposium (SAS), 2009 -
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 -
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 -
Heap Assumptions on Demand pdf
A. Podelski, A. Rybalchenko, and T. Wies
In Proceedings of Computer Aided Verification (CAV), 2008 -
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 -
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 -
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 -
Boolean Heaps pdf
A. Podelski and T. Wies
In Proceedings of Static Analysis Symposium (SAS), 2005
In Workshops
-
RECIPE: Applying Open Domain Question Answering to Privacy Policies pdf
Y. Shvartzshanider, A. Balashankar, T. Wies, and L. Subramanian
In Proceedings of Workshop on Machine Reading for Question Answering@ACL, 2018 -
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 -
(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 -
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
-
Symbolic Shape Analysis pdf
T. Wies
University of Freiburg, Freiburg, Germany, 2009
Technical Reports
-
Consistent Updates for Scalable Microservices pdf
D. Chait-Roth, K.S. Namjoshi, and T. Wies
arXiv Technical Report, abs/2508.048292025 -
Complete Multiparty Session Type Projection with Automata pdf
E. Li, F. Stutz, T. Wies, and D. Zufferey
arXiv Technical Report, abs/2305.170792023 -
Less is more: refinement proofs for probabilistic proofs pdf
K. Jiang, D. Chait-Roth, Z. DeStefano, M. Walfish, and T. Wies
IACR Cryptol. ePrint Arch. Technical Report, 2022/15572022 -
Embedding Hindsight Reasoning in Separation Logic pdf
R. Meyer, T. Wies, and S. Wolff
arXiv Technical Report, abs/2209.136922022 -
A Concurrent Program Logic with a Future and History pdf
R. Meyer, T. Wies, and S. Wolff
arXiv Technical Report, arXiv:2207.023552022 -
Local Reasoning for Global Graph Properties pdf
S. Krishna, A.J. Summers, and T. Wies
arXiv Technical Report, arXiv:1911.086322019 -
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.032722017 -
On Structural Counter Abstraction pdf
K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
NYU Technical Report, TR2012-9472013 -
Automating Separation Logic Using SMT pdf
R. Piskac, T. Wies, and D. Zufferey
NYU Technical Report, TR2013-9542013 -
Complete Instantiation-Based Interpolation pdf
N. Totla and T. Wies
NYU Technical Report, TR2012-9502012 -
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 -
On Deciding Functional Lists with Sublist Sets pdf
T. Wies, M. Mu\~n, and V. Kuncak
EPFL Technical Report, EPFL-REPORT-1483612010 -
On Combining Theories with Shared Set Operations pdf
T. Wies, R. Piskac, and V. Kuncak
EPFL Technical Report, LARA-REPORT-2009-0022009 -
On Set-Driven Combination of Logics and Verifiers pdf
T. Wies and V. Kuncak
EPFL Technical Report, LARA-REPORT-2009-0012009 -
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