Selected Publications

• 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

• Embedding Hindsight Reasoning in Separation Logic pdf

  R. Meyer, T. Wies, and S. Wolff
  To appear in 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

• 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

• Automated Verification of Concurrent Search Structures pdf

  S. Krishna, N. Patel, D. Shasha, and T. Wies
  Morgan & Claypool Publishers, 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

• 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

• 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

• 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

• 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

• 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.

• 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.

Organizer

• 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

• POPL 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

Books

1. Automated Verification of Concurrent Search Structures pdf

   S. Krishna, N. Patel, D. Shasha, and T. Wies
   Morgan & Claypool Publishers, 2021

In Journals

2. Embedding Hindsight Reasoning in Separation Logic pdf

   R. Meyer, T. Wies, and S. Wolff
   To appear in PACMPL, 7(Programming Language Design and Implementation (PLDI)), 2023

3. 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

4. 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

5. 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

6. 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

7. Complete Instantiation-Based Interpolation pdf

   N. Totla and T. Wies
   Journal of Automated Reasoning, 57(1), 2016

8. Preface - Invariant Generation pdf

   G. Grov and T. Wies
   Science of Computer Programming (SCICO), 93, 2014

9. 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

10. 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

11. nekton: a linearizability proof checker pdf

    R. Meyer, A. Opaterny, T. Wies, and S. Wolff
    In Proceedings of Computer Aided Verification (CAV), 2023

12. 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

13. 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

14. 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

15. 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

16. TarTar: A Timed Automata Repair Tool pdf

    M. Kölbl, S. Leue, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2020

17. 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

18. 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

19. 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

20. Clock Bound Repair for Timed Systems pdf

    M. Kölbl, S. Leue, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2019

21. 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

22. 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

23. 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

24. 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

25. 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

26. Classifying Bugs with Interpolants pdf

    A. Podelski, M. Schäf, and T. Wies
    In Proceedings of Tests and Proofs (TAP), 2016

27. 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

28. 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

29. 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

30. 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

31. 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

32. 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

33. Automating Separation Logic with Trees and Data pdf

    R. Piskac, T. Wies, and D. Zufferey
    In Proceedings of Computer Aided Verification (CAV), 2014

34. Dynamic Package Interfaces pdf

    S. Esmaeilsabzali, R. Majumdar, T. Wies, and D. Zufferey
    In Proceedings of Fundamental Approaches to Software Engineering (FASE), 2014

35. 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

36. Cascade 2.0 pdf

    W. Wang, C. Barrett, and T. Wies
    In Proceedings of VMCAI, 2014

37. 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

38. Automating Separation Logic using SMT pdf

    R. Piskac, T. Wies, and D. Zufferey
    In Proceedings of Computer Aided Verification (CAV), 2013

39. Structural Counter Abstraction pdf

    K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
    In Proceedings of TACAS, 2013

40. 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

41. Complete Instantiation-Based Interpolation pdf

    N. Totla and T. Wies
    In Proceedings of ACM Symposium on the Principles of Programming Languages (POPL), 2013

42. Error Invariants pdf

    E. Ermis, M. Schäf, and T. Wies
    In Proceedings of Formal Methods (FM), 2012

43. 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

44. 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

45. 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

46. 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

47. Decision Procedures for Automating Termination Proofs pdf

    R. Piskac and T. Wies
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011

48. 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

49. 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

50. 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

51. Counterexample-guided focus pdf slides

    A. Podelski and T. Wies
    In Proceedings of ACM Symposium on the Principles of Programming Languages (POPL), 2010

52. 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

53. 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

54. Abstraction Refinement for Quantified Array Assertions pdf

    M.N. Seghir, A. Podelski, and T. Wies
    In Proceedings of Static Analysis Symposium (SAS), 2009

55. 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

56. 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

57. Heap Assumptions on Demand pdf

    A. Podelski, A. Rybalchenko, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2008

58. 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

59. 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

60. 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

61. Boolean Heaps pdf

    A. Podelski and T. Wies
    In Proceedings of Static Analysis Symposium (SAS), 2005

In Workshops

62. 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

63. 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

64. (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

65. 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

66. Symbolic Shape Analysis pdf

    T. Wies
    University of Freiburg, Freiburg, Germany, 2009

Technical Reports

67. Complete Multiparty Session Type Projection with Automata pdf

    E. Li, F. Stutz, T. Wies, and D. Zufferey
    arXiv Technical Report, abs/2305.170792023

68. 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

69. Embedding Hindsight Reasoning in Separation Logic pdf

    R. Meyer, T. Wies, and S. Wolff
    arXiv Technical Report, abs/2209.136922022

70. A Concurrent Program Logic with a Future and History pdf

    R. Meyer, T. Wies, and S. Wolff
    arXiv Technical Report, arXiv:2207.023552022

71. Local Reasoning for Global Graph Properties pdf

    S. Krishna, A.J. Summers, and T. Wies
    arXiv Technical Report, arXiv:1911.086322019

72. 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

73. On Structural Counter Abstraction pdf

    K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
    NYU Technical Report, TR2012-9472013

74. Automating Separation Logic Using SMT pdf

    R. Piskac, T. Wies, and D. Zufferey
    NYU Technical Report, TR2013-9542013

75. Complete Instantiation-Based Interpolation pdf

    N. Totla and T. Wies
    NYU Technical Report, TR2012-9502012

76. 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

77. On Deciding Functional Lists with Sublist Sets pdf

    T. Wies, M. Mu\~n, and V. Kuncak
    EPFL Technical Report, EPFL-REPORT-1483612010

78. On Combining Theories with Shared Set Operations pdf

    T. Wies, R. Piskac, and V. Kuncak
    EPFL Technical Report, LARA-REPORT-2009-0022009

79. On Set-Driven Combination of Logics and Verifiers pdf

    T. Wies and V. Kuncak
    EPFL Technical Report, LARA-REPORT-2009-0012009

80. 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