Thomas Wies

Henzinger_Thomas Group

23 Publications

Mark all

[23]
2013 | Conference Paper | IST-REx-ID: 2447 | OA
Automating separation logic using SMT
R. Piskac, T. Wies, D. Zufferey, 8044 (2013) 773–789.
[Submitted Version] View | Files available | DOI
 
[22]
2013 | Conference Paper | IST-REx-ID: 2847 | OA
Structural Counter Abstraction
K. Bansal, E. Koskinen, T. Wies, D. Zufferey, 7795 (2013) 62–77.
[Submitted Version] View | Files available | DOI | Download Submitted Version (ext.)
 
[21]
2012 | Conference Paper | IST-REx-ID: 3251 | OA
Ideal abstractions for well structured transition systems
D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460.
[Submitted Version] View | Files available | DOI
 
[20]
2011 | Conference Paper | IST-REx-ID: 3302 | OA
Static scheduling in clouds
T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, USENIX, 2011, pp. 1–6.
[Submitted Version] View | Files available
 
[19]
2011 | Conference Paper | IST-REx-ID: 3324 | OA
Decision procedures for automating termination proofs
R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp. 371–386.
[Submitted Version] View | DOI | Download Submitted Version (ext.)
 
[18]
2011 | Conference Paper | IST-REx-ID: 3358 | OA
Scheduling large jobs by abstraction refinement
T.A. Henzinger, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2011, pp. 329–342.
[Published Version] View | DOI | Download Published Version (ext.)
 
[17]
2011 | Technical Report | IST-REx-ID: 5383 | OA
On an efficient decision procedure for imperative tree data structures
T. Wies, M. Muñiz, V. Kuncak, On an Efficient Decision Procedure for Imperative Tree Data Structures, IST Austria, 2011.
[Published Version] View | Files available | DOI
 
[16]
2011 | Conference Paper | IST-REx-ID: 3323
An efficient decision procedure for imperative tree data structures
T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.
View | Files available | DOI
 
[15]
2010 | Conference Paper | IST-REx-ID: 4364
Counterexample-guided focus
A. Podelski, T. Wies, in:, ACM, 2010, pp. 249–260.
View | DOI
 
[14]
2010 | Conference Paper | IST-REx-ID: 4378 | OA
Building a calculus of data structures
V. Kuncak, R. Piskac, P. Suter, T. Wies, in:, G. Barthe, M. Hermenegildo (Eds.), Springer, 2010, pp. 26–44.
[Submitted Version] View | DOI | Download Submitted Version (ext.)
 
[13]
2010 | Conference Paper | IST-REx-ID: 4381 | OA
FlexPRICE: Flexible provisioning of resources in a cloud environment
T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010, pp. 83–90.
[Submitted Version] View | Files available | DOI
 
[12]
2010 | Conference Paper | IST-REx-ID: 4380 | OA
A marketplace for cloud resources
T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010, pp. 1–8.
[Submitted Version] View | Files available | DOI
 
[11]
2010 | Journal Article | IST-REx-ID: 533
Doomed program points
J. Hoenicke, K. Leino, A. Podelski, M. Schäf, T. Wies, Formal Methods in System Design 37 (2010) 171–199.
View | DOI
 
[10]
2010 | Conference Paper | IST-REx-ID: 4361 | OA
Forward analysis of depth-bounded processes
T. Wies, D. Zufferey, T.A. Henzinger, in:, L. Ong (Ed.), Springer, 2010, pp. 94–108.
[Submitted Version] View | Files available | DOI
 
[9]
2009 | Conference Paper | IST-REx-ID: 4365
Abstraction Refinement for Quantified Array Assertions
M. Seghir, A. Podelski, T. Wies, in:, Springer, 2009, pp. 3–18.
View | DOI
 
[8]
2009 | Conference Paper | IST-REx-ID: 4360
Combining Theories with Shared Set Operations
T. Wies, R. Piskac, V. Kuncak, in:, Springer, 2009, pp. 366–382.
View | DOI
 
[7]
2009 | Conference Paper | IST-REx-ID: 4375
Intra-module Inference
S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, T. Wies, in:, Springer, 2009, pp. 493–508.
View | DOI
 
[6]
2009 | Conference Paper | IST-REx-ID: 4377
It's Doomed; We Can Prove It
J. Hoenicke, K.R. Leino, A. Podelski, M. Schäf, T. Wies, in:, Springer, 2009, pp. 338–353.
View | DOI
 
[5]
2008 | Conference Paper | IST-REx-ID: 4366
Heap Assumptions on Demand
A. Podelski, A. Rybalchenko, T. Wies, in:, Springer, 2008, pp. 314–327.
View | DOI
 
[4]
2007 | Conference Paper | IST-REx-ID: 4394
Using First-Order Theorem Provers in the Jahob Data Structure Verification System
C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, M. Rinard, in:, Springer, 2007, pp. 74–88.
View | DOI
 
[3]
2007 | Conference Paper | IST-REx-ID: 4398
Shape Analysis for Composite Data Structures
J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O’Hearn, T. Wies, H. Yang, in:, Springer, 2007, pp. 178–192.
View | DOI
 
[2]
2006 | Conference Paper | IST-REx-ID: 4359
Field Constraint Analysis
T. Wies, V. Kuncak, P. Lam, A. Podelski, M. Rinard, in:, Springer, 2006, pp. 157–173.
View | DOI
 
[1]
2005 | Conference Paper | IST-REx-ID: 4367
Boolean Heaps
A. Podelski, T. Wies, in:, Springer, 2005, pp. 267–282.
View | DOI
 
Marked Publication(s)

Search

Filter Publications

    • Display / Sort

    Export / Embed

23 Publications

Mark all

[23]
2013 | Conference Paper | IST-REx-ID: 2447 | OA
Automating separation logic using SMT
R. Piskac, T. Wies, D. Zufferey, 8044 (2013) 773–789.
[Submitted Version] View | Files available | DOI
 
[22]
2013 | Conference Paper | IST-REx-ID: 2847 | OA
Structural Counter Abstraction
K. Bansal, E. Koskinen, T. Wies, D. Zufferey, 7795 (2013) 62–77.
[Submitted Version] View | Files available | DOI | Download Submitted Version (ext.)
 
[21]
2012 | Conference Paper | IST-REx-ID: 3251 | OA
Ideal abstractions for well structured transition systems
D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460.
[Submitted Version] View | Files available | DOI
 
[20]
2011 | Conference Paper | IST-REx-ID: 3302 | OA
Static scheduling in clouds
T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, USENIX, 2011, pp. 1–6.
[Submitted Version] View | Files available
 
[19]
2011 | Conference Paper | IST-REx-ID: 3324 | OA
Decision procedures for automating termination proofs
R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp. 371–386.
[Submitted Version] View | DOI | Download Submitted Version (ext.)
 
[18]
2011 | Conference Paper | IST-REx-ID: 3358 | OA
Scheduling large jobs by abstraction refinement
T.A. Henzinger, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2011, pp. 329–342.
[Published Version] View | DOI | Download Published Version (ext.)
 
[17]
2011 | Technical Report | IST-REx-ID: 5383 | OA
On an efficient decision procedure for imperative tree data structures
T. Wies, M. Muñiz, V. Kuncak, On an Efficient Decision Procedure for Imperative Tree Data Structures, IST Austria, 2011.
[Published Version] View | Files available | DOI
 
[16]
2011 | Conference Paper | IST-REx-ID: 3323
An efficient decision procedure for imperative tree data structures
T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.
View | Files available | DOI
 
[15]
2010 | Conference Paper | IST-REx-ID: 4364
Counterexample-guided focus
A. Podelski, T. Wies, in:, ACM, 2010, pp. 249–260.
View | DOI
 
[14]
2010 | Conference Paper | IST-REx-ID: 4378 | OA
Building a calculus of data structures
V. Kuncak, R. Piskac, P. Suter, T. Wies, in:, G. Barthe, M. Hermenegildo (Eds.), Springer, 2010, pp. 26–44.
[Submitted Version] View | DOI | Download Submitted Version (ext.)
 
[13]
2010 | Conference Paper | IST-REx-ID: 4381 | OA
FlexPRICE: Flexible provisioning of resources in a cloud environment
T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010, pp. 83–90.
[Submitted Version] View | Files available | DOI
 
[12]
2010 | Conference Paper | IST-REx-ID: 4380 | OA
A marketplace for cloud resources
T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010, pp. 1–8.
[Submitted Version] View | Files available | DOI
 
[11]
2010 | Journal Article | IST-REx-ID: 533
Doomed program points
J. Hoenicke, K. Leino, A. Podelski, M. Schäf, T. Wies, Formal Methods in System Design 37 (2010) 171–199.
View | DOI
 
[10]
2010 | Conference Paper | IST-REx-ID: 4361 | OA
Forward analysis of depth-bounded processes
T. Wies, D. Zufferey, T.A. Henzinger, in:, L. Ong (Ed.), Springer, 2010, pp. 94–108.
[Submitted Version] View | Files available | DOI
 
[9]
2009 | Conference Paper | IST-REx-ID: 4365
Abstraction Refinement for Quantified Array Assertions
M. Seghir, A. Podelski, T. Wies, in:, Springer, 2009, pp. 3–18.
View | DOI
 
[8]
2009 | Conference Paper | IST-REx-ID: 4360
Combining Theories with Shared Set Operations
T. Wies, R. Piskac, V. Kuncak, in:, Springer, 2009, pp. 366–382.
View | DOI
 
[7]
2009 | Conference Paper | IST-REx-ID: 4375
Intra-module Inference
S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, T. Wies, in:, Springer, 2009, pp. 493–508.
View | DOI
 
[6]
2009 | Conference Paper | IST-REx-ID: 4377
It's Doomed; We Can Prove It
J. Hoenicke, K.R. Leino, A. Podelski, M. Schäf, T. Wies, in:, Springer, 2009, pp. 338–353.
View | DOI
 
[5]
2008 | Conference Paper | IST-REx-ID: 4366
Heap Assumptions on Demand
A. Podelski, A. Rybalchenko, T. Wies, in:, Springer, 2008, pp. 314–327.
View | DOI
 
[4]
2007 | Conference Paper | IST-REx-ID: 4394
Using First-Order Theorem Provers in the Jahob Data Structure Verification System
C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, M. Rinard, in:, Springer, 2007, pp. 74–88.
View | DOI
 
[3]
2007 | Conference Paper | IST-REx-ID: 4398
Shape Analysis for Composite Data Structures
J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O’Hearn, T. Wies, H. Yang, in:, Springer, 2007, pp. 178–192.
View | DOI
 
[2]
2006 | Conference Paper | IST-REx-ID: 4359
Field Constraint Analysis
T. Wies, V. Kuncak, P. Lam, A. Podelski, M. Rinard, in:, Springer, 2006, pp. 157–173.
View | DOI
 
[1]
2005 | Conference Paper | IST-REx-ID: 4367
Boolean Heaps
A. Podelski, T. Wies, in:, Springer, 2005, pp. 267–282.
View | DOI
 
Marked Publication(s)

Search

Filter Publications

    • Display / Sort

    Export / Embed