Thomas Wies

Computer Science Department
Courant Institute of Mathematical Sciences
New York University

Publications

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

In Conferences

  1. VERMEER: A Tool for Tracing and Explaining Faulty C Programs with Daniel Schwartz-Narbonne, Chanseok Oh, and Martin Schäf
    To appear in Proceedings of ICSE, Demonstrations Track, 2015.
  2. Conflict-Directed Graph Coverage with Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanović, and Philipp Rümmer
    To appear in Proceedings of NFM, 2015. [pdf]
  3. Finding Minimum Type Error Sources with Zvonimir Pavlinovic and Tim King
    In Proceedings of OOPSLA, 2014. Best Paper Award. [pdf]
  4. Concolic Fault Abstraction with Chanseok Oh, Martin Schäf, and Daniel Schwartz-Narbonne
    In Proceedings of SCAM, 2014. [pdf]
  5. Automating Separation Logic with Trees and Data with Ruzica Piskac and Damien Zufferey
    In Proceedings of CAV, 2014. [pdf]
  6. GRASShopper: Complete Heap Verification with Mixed Specifications with Ruzica Piskac and Damien Zufferey
    In Proceedings of TACAS, 2014. [pdf]
  7. Dynamic Package Interfaces with Shahram Esmaeilsabzali, Rupak Majumdar, and Damien Zufferey
    In Proceedings of FASE, 2014. [pdf]
  8. Cascade 2.0 with Wei Wang and Clark Barrett
    In Proceedings of VMCAI, 2014. [pdf]
  9. Explaining Inconsistent Code with Martin Schäf and Daniel Schwartz-Narbonne
    In Proceedings of ESEC/FSE, 2013. [pdf]
  10. Automating Separation Logic using SMT with Ruzica Piskac and Damien Zufferey
    In Proceedings of CAV, 2013. [pdf] [pdf-extended]
  11. Structural Counter Abstraction with Kshitij Bansal, Eric Koskinen, and Damien Zufferey
    In Proceedings of TACAS, 2013. [pdf] [pdf-extended]
  12. Complete Instantiation-Based Interpolation with Nishant Totla
    In Proceedings of POPL, 2013. [pdf] [pdf-extended]
  13. Flow-Sensitive Fault Localization with Jürgen Christ, Evren Ermis, and Martin Schäf
    In Proceedings of VMCAI, 2013. [pdf]
  14. Error Invariants with Evren Ermis and Martin Schäf
    In Proceedings of FM, 2012. [pdf]
  15. Ideal Abstractions for Well-Structured Transition Systems with Damien Zufferey and Thomas A. Henzinger
    In Proceedings of VMCAI, 2012. [pdf]
  16. Deciding Functional Lists with Sublist Sets with Marco Muñiz and Viktor Kuncak
    In Proceedings of VSTTE, 2012. [pdf] [pdf-extended]
  17. An Efficient Decision Procedure for Imperative Tree Data Structures with Marco Muñiz and Viktor Kuncak
    In Proceedings of CADE, 2011. [pdf] [pdf-extended]
  18. Scheduling Large Jobs by Abstraction Refinement with Thomas A. Henzinger, Vasu Singh, and Damien Zufferey
    In Proceedings of EuroSys, 2011. [pdf]
  19. Decision Procedures for Automating Termination Proofs with Ruzica Piskac
    In Proceedings of VMCAI, 2011. [pdf]
  20. A Marketplace for Cloud Resources with Thomas A. Henzinger, Vasu Singh, Anmol Tomar, and Damien Zufferey
    In Proceedings of EMSOFT, 2010. [pdf]
  21. FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment with Thomas A. Henzinger, Vasu Singh, Anmol Tomar, and Damien Zufferey
    In Proceedings of IEEE CLOUD, 2010. [pdf]
  22. Forward Analysis of Depth-Bounded Processes with Damien Zufferey and Thomas A. Henzinger
    In Proceedings of FoSSaCS, 2010. [pdf]
  23. Counterexample-Guided Focus with Andreas Podelski
    In Proceedings of POPL, 2010. [pdf] [ppt-slides]
  24. Building a Calculus of Data Structures with Viktor Kuncak, Ruzica Piskac, and Philippe Suter
    In Proceedings of VMCAI, 2010. [pdf]
  25. It's doomed; we can prove it with Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, and Martin Schäf
    In Proceedings of FM, 2009. [pdf]
  26. Combining Theories with Shared Set Operations with Ruzica Piskac and Viktor Kuncak
    In Proceedings of FroCoS, 2009. [pdf] [pdf-extended] [ppt-slides]
  27. Abstraction Refinement for Quantified Array Assertions with Nassim Seghir and Andreas Podelski
    In Proceedings of SAS, 2009. [pdf]
  28. Intra-module Inference with Shuvendu Lahiri, Shaz Qadeer, Juan Galeotti, and Jan Voung
    In Proceedings of CAV, 2009. [pdf]
  29. Heap Assumptions on Demand with Andreas Podelski and Andrey Rybalchenko
    In Proceedings of CAV, 2008. [pdf] [pdf-extended]
  30. Shape analysis for composite data structures with Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, and Hongseok Yang
    In Proceedings of CAV, 2007. [pdf]
  31. Using First-Order Theorem Provers in the Jahob Data Structure Verification System with Charles Bouillaguet, Viktor Kuncak, Karen Zee, and Martin Rinard
    In Proceedings of VMCAI, 2007. [pdf]
  32. Field Constraint Analysis with Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard
    In Proceedings of VMCAI, 2006. [pdf] [pdf-extended] [pdf-slides]
  33. Boolean Heaps with Andreas Podelski
    In Proceedings of SAS, 2005. [pdf] [pdf-slides]

In Journals

  1. Preface - Invariant Generation with Gudmund Grov
    Science of Computer Programming (SCICO). 93, 2014.
  2. Doomed Program Points with Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, and Martin Schäf
    Formal Methods in System Design (FMSD). 37(2):171, 2010. [pdf]

In Workshops

  1. Static Scheduling in Clouds with Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, and Damien Zufferey
    In Proceedings of HotCloud, 2011. [pdf]
  2. (EC)2 in EC2 with Thomas A. Henzinger, Vasu Singh, Anmol Tomar, and Damien Zufferey
    (EC)2 Workshop, 2010. [pdf]
  3. Verifying Complex Properties using Symbolic Shape Analysis with Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard
    Workshop on Heap Abstraction and Verification, March 2007. [pdf]

Thesis

  1. Symbolic Shape Analysis
    PhD Thesis, University of Freiburg, Freiburg, Germany, 2009. [pdf]

Technical Reports

  1. Automating Separation Logic using SMT with Ruzica Piskac and Damien Zufferey
    NYU Technical Report TR2013-954, March, 2013. [pdf]
  2. Complete Instantiation-Based Interpolation with Nishant Totla
    NYU Technical Report TR2012-950, July, 2012. [pdf]
  3. Structural Counter Abstraction with Kshitij Bansal, Eric Koskinen, and Damien Zufferey
    NYU Technical Report TR2012-947, April, 2012. [pdf]
  4. On an Efficient Decision Procedure for Imperative Tree Data Structures with Marco Muñiz and Viktor Kuncak
    IST Technical Report IST-2011-0005, April, 2011. [pdf]
  5. On Deciding Functional Lists with Sublist Sets with Marco Muñiz and Viktor Kuncak
    EPFL Technical Report EPFL-REPORT-148361, April, 2010. [pdf]
  6. On Combining Theories with Shared Set Operations with Ruzica Piskac and Viktor Kuncak
    EPFL Technical Report LARA-REPORT-2009-002. February, 2009. [pdf]
  7. On Set-Driven Combination of Logics and Verifiers with Viktor Kuncak
    EPFL Technical Report LARA-REPORT-2009-001. 2009. [pdf]
  8. On Verifying Complex Properties using Symbolic Shape Analysis with Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard
    Max-Planck Institute for Computer Science Technical Report MPI-I-2006-2-1. 2006 [pdf]
  9. On Field Constraint Analysis with Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard
    MIT CSAIL Technical Report MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010. 2005. [pdf]