BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Cyprus
1 × Germany
1 × Poland
1 × The Netherlands
1 × United Kingdom
2 × Canada
2 × Russia
2 × Spain
4 × Italy
5 × France
8 × USA
Collaborated with:
D.Zufferey A.Podelski R.Piskac M.Schäf V.Kuncak T.King D.Schwartz-Narbonne Z.Pavlinovic T.A.Henzinger E.Ermis C.Oh N.Totla K.Bansal M.C.Rinard W.Wang C.Barrett M.Muñiz M.N.Seghir A.Rybalchenko M.Kölbl S.Leue Siddharth Krishna Dennis E. Shasha S.Esmaeilsabzali R.Majumdar E.Koskinen J.Christ P.Suter A.Reynolds C.W.Barrett S.K.Lahiri S.Qadeer J.P.Galeotti J.W.Voung J.Hoenicke K.R.M.Leino C.Bouillaguet K.Zee P.Lam J.Berdine C.Calcagno B.Cook D.Distefano P.W.O'Hearn H.Yang
Talks about:
structur (7) data (6) abstract (4) local (4) analysi (3) system (3) error (3) autom (3) heap (3) procedur (2)

Person: Thomas Wies

DBLP DBLP: Wies:Thomas

Contributed to:

CAV 20152015
ICFP 20152015
ICSE 20152015
CAV 20142014
FASE 20142014
OOPSLA 20142014
SCAM 20142014
TACAS 20142014
VMCAI 20142014
CAV 20132013
ESEC/FSE 20132013
POPL 20132013
TACAS 20132013
VMCAI 20132013
FM 20122012
VMCAI 20122012
CADE 20112011
VMCAI 20112011
FOSSACS 20102010
POPL 20102010
VMCAI 20102010
CAV 20092009
FM 20092009
SAS 20092009
CAV 20082008
CAV 20072007
VMCAI 20072007
VMCAI 20062006
SAS 20052005
CAV (1) 20192019
POPL 20182018

Wrote 31 papers:

Deciding Local Theory Extensions via E-matching (KB, AR, TK, CWB, TW), pp. 87–105.
ICFP-2015-Pavlinovic0W #fault #locality #smt
Practical SMT-based type error localization (ZP, TK, TW), pp. 412–423.
ICSE-v2-2015-Schwartz-Narbonne #c #named #source code
VERMEER: A Tool for Tracing and Explaining Faulty C Programs (DSN, CO, MS, TW), pp. 737–740.
CAV-2014-PiskacWZ #automation #logic
Automating Separation Logic with Trees and Data (RP, TW, DZ), pp. 711–728.
FASE-2014-EsmaeilsabzaliMWZ #interface
Dynamic Package Interfaces (SE, RM, TW, DZ), pp. 261–275.
OOPSLA-2014-PavlinovicKW #fault
Finding minimum type error sources (ZP, TK, TW), pp. 525–542.
SCAM-2014-OhSSW #fault #locality
Concolic Fault Localization (CO, MS, DSN, TW), pp. 135–144.
TACAS-2014-PiskacWZ #named #specification #verification
GRASShopper — Complete Heap Verification with Mixed Specifications (RP, TW, DZ), pp. 124–139.
Cascade 2.0 (WW, CB, TW), pp. 142–160.
CAV-2013-PiskacWZ #automation #logic #smt #using
Automating Separation Logic Using SMT (RP, TW, DZ), pp. 773–789.
ESEC-FSE-2013-SchafSW #consistency
Explaining inconsistent code (MS, DSN, TW), pp. 521–531.
Complete instantiation-based interpolation (NT, TW), pp. 537–548.
TACAS-2013-BansalKWZ #abstraction
Structural Counter Abstraction (KB, EK, TW, DZ), pp. 62–77.
VMCAI-2013-ChristESW #fault #locality
Flow-Sensitive Fault Localization (JC, EE, MS, TW), pp. 189–208.
FM-2012-ErmisSW #fault #invariant
Error Invariants (EE, MS, TW), pp. 187–201.
VMCAI-2012-ZuffereyWH #abstraction
Ideal Abstractions for Well-Structured Transition Systems (DZ, TW, TAH), pp. 445–460.
CADE-2011-WiesMK #data type #imperative #performance
An Efficient Decision Procedure for Imperative Tree Data Structures (TW, MM, VK), pp. 476–491.
VMCAI-2011-PiskacW #automation #proving #termination
Decision Procedures for Automating Termination Proofs (RP, TW), pp. 371–386.
FoSSaCS-2010-WiesZH #analysis #bound #process
Forward Analysis of Depth-Bounded Processes (TW, DZ, TAH), pp. 94–108.
Counterexample-guided focus (AP, TW), pp. 249–260.
VMCAI-2010-KuncakPSW #calculus #data type
Building a Calculus of Data Structures (VK, RP, PS, TW), pp. 26–44.
Intra-module Inference (SKL, SQ, JPG, JWV, TW), pp. 493–508.
It’s Doomed; We Can Prove It (JH, KRML, AP, MS, TW), pp. 338–353.
SAS-2009-SeghirPW #abstraction #array #quantifier #refinement
Abstraction Refinement for Quantified Array Assertions (MNS, AP, TW), pp. 3–18.
Heap Assumptions on Demand (AP, AR, TW), pp. 314–327.
CAV-2007-BerdineCCDOWY #analysis #data type
Shape Analysis for Composite Data Structures (JB, CC, BC, DD, PWO, TW, HY), pp. 178–192.
VMCAI-2007-BouillaguetKWZR #data type #first-order #proving #theorem proving #using #verification
Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.
VMCAI-2006-WiesKLPR #analysis #constraints
Field Constraint Analysis (TW, VK, PL, AP, MCR), pp. 157–173.
Boolean Heaps (AP, TW), pp. 268–283.
CAV-2019-KolblLW #bound
Clock Bound Repair for Timed Systems (MK, SL, TW), pp. 79–96.
POPL-2018-KrishnaSW #abstraction #composition #concurrent #data type
Go with the flow: compositional abstractions for concurrent data structures (SK, DES, TW), p. 31.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.