Thomas Wies: Homepage

Thomas Wies: Homepage
New York
University
COURANT
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.
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
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
Implementability of Global Distributed Protocols modulo Network Architectures
E. Li and T. Wies
To appear in
PACMPL,
10(Programming Laguage Design and Implementaion (PLDI))
2026
Consistent Updates for Scalable Microservices
pdf
D. Chait-Roth, K.S. Namjoshi, and T. Wies
PACMPL,
10(Principles of Programming Languages (POPL))
2026
The Privacy Quagmire: Bridging Computer Science and Legal Nuance
pdf
Y. Zhao, V. Chandrasekaran, T. Wies, and L. Subramanian
In Proceedings of
ACM Workshop on Hot Topics in Networks (HOTNETS)
, 2025
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
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
Complete list of publications
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)
Fall 2023
Fall 2021
Fall 2016
Fall 2015
Spring 2015
Programming Languages (graduate)
Fall 2022
Spring 2019
Fall 2018
Fall 2012
Computer Systems Organization (undergraduate)
Fall 2019
Object-Oriented Programming (graduate)
Spring 2018
Object-Oriented Programming (undergraduate)
Fall 2017
Spring 2017
Fall 2013
Rigorous Software Development (graduate)
Spring 2016
Spring 2013
Spring 2012
Programming Paradigms for Concurrency (graduate)
Spring 2014
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
Implementability of Global Distributed Protocols modulo Network Architectures
E. Li and T. Wies
To appear in
PACMPL,
10(Programming Laguage Design and Implementaion (PLDI))
2026
Consistent Updates for Scalable Microservices
pdf
D. Chait-Roth, K.S. Namjoshi, and T. Wies
PACMPL,
10(Principles of Programming Languages (POPL))
2026
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
The Privacy Quagmire: Bridging Computer Science and Legal Nuance
pdf
Y. Zhao, V. Chandrasekaran, T. Wies, and L. Subramanian
In Proceedings of
ACM Workshop on Hot Topics in Networks (HOTNETS)
, 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
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
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