Boolean Heaps. - Andreas Podelski; Thomas Wies (SAS, 2005)

Field Constraint Analysis. - Thomas Wies; Viktor Kuncak; Patrick Lam 001; Andreas Podelski; Martin C. Rinard (VMCAI, 2006)

On Verifying Complex Properties using Symbolic Shape Analysis - Thomas Wies; Viktor Kuncak; Karen Zee; Andreas Podelski; Martin C. Rinard (CoRR, 2006)

Shape Analysis for Composite Data Structures. - Josh Berdine; Cristiano Calcagno; Byron Cook; Dino Distefano; Peter W. O'Hearn; Thomas Wies; Hongseok Yang (CAV, 2007)

Using First-Order Theorem Provers in the Jahob Data Structure Verification System. - Charles Bouillaguet; Viktor Kuncak; Thomas Wies; Karen Zee; Martin C. Rinard (VMCAI, 2007)

Heap Assumptions on Demand. - Andreas Podelski; Andrey Rybalchenko; Thomas Wies (CAV, 2008)

Intra-module Inference. - Shuvendu K. Lahiri; Shaz Qadeer; Juan P. Galeotti; Jan W. Voung; Thomas Wies (CAV, 2009)

It's Doomed; We Can Prove It. - Jochen Hoenicke; K. Rustan M. Leino; Andreas Podelski; Martin Schäf; Thomas Wies (FM, 2009)

Combining Theories with Shared Set Operations. - Thomas Wies; Ruzica Piskac; Viktor Kuncak (FroCoS, 2009)

Abstraction Refinement for Quantified Array Assertions. - Mohamed Nassim Seghir; Andreas Podelski; Thomas Wies (SAS, 2009)

Symbolic shape analysis. - Thomas Wies (2009)

FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment. - Thomas A. Henzinger; Anmol V. Singh; Vasu Singh; Thomas Wies; Damien Zufferey (IEEE CLOUD, 2010)

A marketplace for cloud resources. - Thomas A. Henzinger; Anmol V. Singh; Vasu Singh; Thomas Wies; Damien Zufferey (EMSOFT, 2010)

Forward Analysis of Depth-Bounded Processes. - Thomas Wies; Damien Zufferey; Thomas A. Henzinger (FoSSaCS, 2010)

Counterexample-guided focus. - Andreas Podelski; Thomas Wies (POPL, 2010)

Building a Calculus of Data Structures. - Viktor Kuncak; Ruzica Piskac; Philippe Suter; Thomas Wies (VMCAI, 2010)

Doomed program points. - Jochen Hoenicke; K. Rustan M. Leino; Andreas Podelski; Martin Schäf; Thomas Wies (Formal Methods Syst. Des., 2010)

An Efficient Decision Procedure for Imperative Tree Data Structures. - Thomas Wies; Marco Muñiz; Viktor Kuncak (CADE, 2011)

Scheduling large jobs by abstraction refinement. - Thomas A. Henzinger; Vasu Singh; Thomas Wies; Damien Zufferey (EuroSys, 2011)

Static Scheduling in Clouds. - Thomas A. Henzinger; Anmol V. Singh; Vasu Singh; Thomas Wies; Damien Zufferey (HotCloud, 2011)

Decision Procedures for Automating Termination Proofs. - Ruzica Piskac; Thomas Wies (VMCAI, 2011)

Error Invariants. - Evren Ermis; Martin Schäf; Thomas Wies (FM, 2012)

Ideal Abstractions for Well-Structured Transition Systems. - Damien Zufferey; Thomas Wies; Thomas A. Henzinger (VMCAI, 2012)

Deciding Functional Lists with Sublist Sets. - Thomas Wies; Marco Muñiz; Viktor Kuncak (VSTTE, 2012)

Automating Separation Logic Using SMT. - Ruzica Piskac; Thomas Wies; Damien Zufferey (CAV, 2013)

Explaining inconsistent code. - Martin Schäf; Daniel Schwartz-Narbonne; Thomas Wies (ESEC/SIGSOFT FSE, 2013)

Structural Counter Abstraction. - Kshitij Bansal; Eric Koskinen; Thomas Wies; Damien Zufferey (TACAS, 2013)

Flow-Sensitive Fault Localization. - Jürgen Christ; Evren Ermis; Martin Schäf; Thomas Wies (VMCAI, 2013)

A Notion of Dynamic Interface for Depth-Bounded Object-Oriented Packages. - Shahram Esmaeilsabzali; Rupak Majumdar; Thomas Wies; Damien Zufferey (CoRR, 2013)

Dynamic Package Interfaces - Extended Version. - Shahram Esmaeilsabzali; Rupak Majumdar; Thomas Wies; Damien Zufferey (CoRR, 2013)

Automating Separation Logic with Trees and Data. - Ruzica Piskac; Thomas Wies; Damien Zufferey (CAV, 2014)

Dynamic Package Interfaces. - Shahram Esmaeilsabzali; Rupak Majumdar; Thomas Wies; Damien Zufferey (FASE, 2014)

Concolic Fault Localization. - Chanseok Oh; Martin Schäf; Daniel Schwartz-Narbonne; Thomas Wies (SCAM, 2014)

GRASShopper - Complete Heap Verification with Mixed Specifications. - Ruzica Piskac; Thomas Wies; Damien Zufferey (TACAS, 2014)

Cascade 2.0. - Wei Wang 062; Clark W. Barrett; Thomas Wies (VMCAI, 2014)

Preface - Invariant Generation. - Gudmund Grov; Thomas Wies (Sci. Comput. Program., 2014)

Deciding Local Theory Extensions via E-matching. - Kshitij Bansal; Andrew Reynolds 001; Tim King 001; Clark W. Barrett; Thomas Wies (CAV (2), 2015)

Practical SMT-based type error localization. - Zvonimir Pavlinovic; Tim King 001; Thomas Wies (ICFP, 2015)

VERMEER: A Tool for Tracing and Explaining Faulty C Programs. - Daniel Schwartz-Narbonne; Chanseok Oh; Martin Schäf; Thomas Wies (ICSE (2), 2015)

Conflict-Directed Graph Coverage. - Daniel Schwartz-Narbonne; Martin Schäf; Dejan Jovanovic; Philipp Rümmer; Thomas Wies (NFM, 2015)

Finding Minimum Type Error Sources. - Zvonimir Pavlinovic; Tim King 001; Thomas Wies (Software Engineering & Management, 2015)

Learning Invariants using Decision Trees. - Siddharth Krishna 001; Christian Puhrsch; Thomas Wies (CoRR, 2015)

Error Invariants for Concurrent Traces. - Andreas Holzer; Daniel Schwartz-Narbonne; Mitra Tabaei Befrouei; Georg Weissenbacher; Thomas Wies (FM, 2016)

Learning Privacy Expectations by Crowdsourcing Contextual Informational Norms. - Yan Shvartzshnaider; Schrasing Tong; Thomas Wies; Paula Kift; Helen Nissenbaum; Lakshminarayanan Subramanian; Prateek Mittal (HCOMP, 2016)

Classifying Bugs with Interpolants. - Andreas Podelski; Martin Schäf; Thomas Wies (TAP@STAF, 2016)

Crowdsourcing Verifiable Contextual Integrity Norms. - Yan Shvartzshnaider; Schrasing Tong; Thomas Wies; Paula Kift; Helen Nissenbaum; Lakshminarayanan Subramanian; Prateek Mittal (CoRR, 2016)

Complete Instantiation-Based Interpolation. - Nishant Totla; Thomas Wies (J. Autom. Reason., 2016)

Partitioned Memory Models for Program Analysis. - Wei Wang 062; Clark W. Barrett; Thomas Wies (VMCAI, 2017)

The VACCINE Framework for Building DLP Systems. - Yan Shvartzshnaider; Zvonimir Pavlinovic; Thomas Wies; Lakshminarayanan Subramanian; Prateek Mittal; Helen Nissenbaum (CoRR, 2017)

Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version). - Siddharth Krishna 001; Dennis E. Shasha; Thomas Wies (CoRR, 2017)

Full accounting for verifiable outsourcing. - Riad S. Wahby; Ye Ji; Andrew J. Blumberg; Abhi Shelat; Justin Thaler; Michael Walfish; Thomas Wies (IACR Cryptol. ePrint Arch., 2017)

RECIPE: Applying Open Domain Question Answering to Privacy Policies. - Yan Shvartzshanider; Ananth Balashankar; Thomas Wies; Lakshminarayanan Subramanian (QA@ACL, 2018)

Go with the flow: compositional abstractions for concurrent data structures. - Siddharth Krishna 001; Dennis E. Shasha; Thomas Wies (Proc. ACM Program. Lang., 2018)

Clock Bound Repair for Timed Systems. - Martin Kölbl; Stefan Leue; Thomas Wies (CAV (1), 2019)

Charting a Course Through Uncertain Environments: SEA Uses Past Problems to Avoid Future Failures. - Preston Moore; Justin Cappos; Phyllis G. Frankl; Thomas Wies (ISSRE, 2019)

VACCINE: Using Contextual Integrity For Data Leakage Detection. - Yan Shvartzshnaider; Zvonimir Pavlinovic; Ananth Balashankar; Thomas Wies; Lakshminarayanan Subramanian; Helen Nissenbaum; Prateek Mittal (WWW, 2019)

TarTar: A Timed Automata Repair Tool. - Martin Kölbl; Stefan Leue; Thomas Wies (CAV (1), 2020)

Local Reasoning for Global Graph Properties. - Siddharth Krishna 001; Alexander J. Summers; Thomas Wies (ESOP, 2020)

Verifying concurrent search structure templates. - Siddharth Krishna 001; Nisarg Patel; Dennis E. Shasha; Thomas Wies (PLDI, 2020)

Beyond The Text: Analysis of Privacy Statements through Syntactic and Semantic Role Labeling. - Yan Shvartzshnaider; Ananth Balashankar; Vikas Patidar; Thomas Wies; Lakshminarayanan Subramanian (CoRR, 2020)

Inverse-Weighted Survival Games. - Xintian Han; Mark Goldstein; Aahlad Manas Puli; Thomas Wies; Adler J. Perotte; Rajesh Ranganath (NeurIPS, 2021)

Automated repair for timed systems. - Martin Kölbl; Stefan Leue; Thomas Wies (Formal Methods Syst. Des., 2021)

Verifying concurrent multicopy search structures. - Nisarg Patel; Siddharth Krishna 001; Dennis E. Shasha; Thomas Wies (Proc. ACM Program. Lang., 2021)

Data flow refinement type inference. - Zvonimir Pavlinovic; Yusen Su; Thomas Wies (Proc. ACM Program. Lang., 2021)

Automated Verification of Concurrent Search Structures - Siddharth Krishna 001; Nisarg Patel; Dennis E. Shasha; Thomas Wies (Morgan & Claypool Publishers, 2021)

Needles in a Haystack: Using PORT to Catch Bad Behaviors within Application Recordings. - Preston Moore; Thomas Wies; Marc Waldman; Phyllis G. Frankl; Justin Cappos (ICSOFT, 2022)

Less is more: refinement proofs for probabilistic proofs. - Kunming Jiang; Devora Chait-Roth; Zachary DeStefano; Michael Walfish; Thomas Wies (IACR Cryptol. ePrint Arch., 2022)

A concurrent program logic with a future and history. - Roland Meyer 001; Thomas Wies; Sebastian Wolff 001 (Proc. ACM Program. Lang., 2022)

Complete Multiparty Session Type Projection with Automata. - Elaine Li; Felix Stutz; Thomas Wies; Damien Zufferey (CAV (3), 2023)

nekton: A Linearizability Proof Checker. - Roland Meyer 001; Anton Opaterny; Thomas Wies; Sebastian Wolff 001 (CAV (1), 2023)

Make Flows Small Again: Revisiting the Flow Framework. - Roland Meyer 001; Thomas Wies; Sebastian Wolff 001 (TACAS (1), 2023)

Context-Aware Separation Logic. - Roland Meyer 001; Thomas Wies; Sebastian Wolff 001 (CoRR, 2023)

Embedding Hindsight Reasoning in Separation Logic. - Roland Meyer 001; Thomas Wies; Sebastian Wolff 001 (Proc. ACM Program. Lang., 2023)

Verifying Concurrent Search Structures (Invited Talk). - Thomas Wies (CONCUR, 2024)

Verifying Lock-Free Search Structure Templates. - Nisarg Patel; Dennis Shasha; Thomas Wies (ECOOP, 2024)

Deciding Subtyping for Asynchronous Multiparty Sessions. - Elaine Li; Felix Stutz; Thomas Wies (ESOP (1), 2024)

Inferring Accumulative Effects of Higher Order Programs. - Mihai Nicola; Chaitanya Agarwal; Eric Koskinen; Thomas Wies (CoRR, 2024)

Verifying Lock-Free Search Structure Templates (Artifact). - Nisarg Patel; Dennis Shasha; Thomas Wies (Dagstuhl Artifacts Ser., 2024)

Raven: An SMT-Based Concurrency Verifier. - Ekanshdeep Gupta; Nisarg Patel; Thomas Wies (CAV (1), 2025)

Sprout: A Verifier for Symbolic Multiparty Protocols. - Elaine Li; Felix Stutz; Thomas Wies; Damien Zufferey (CAV (3), 2025)

Arithmetizing Shape Analysis. - Sebastian Wolff 001; Ekanshdeep Gupta; Zafer Esen; Hossein Hojjat; Philipp Rümmer; Thomas Wies (CAV (1), 2025)

Characterizing Implementability of Global Protocols with Infinite States and Data. - Elaine Li; Felix Stutz; Thomas Wies; Damien Zufferey (Proc. ACM Program. Lang., 2025)

Consistent Updates for Scalable Microservices. - Devora Chait-Roth; Kedar S. Namjoshi; Thomas Wies (CoRR, 2025)