Thomas Wies
Henzinger_Thomas Group
23 Publications
2013 | Conference Paper | IST-REx-ID: 2447 | 
Piskac, R., Wies, T., & Zufferey, D. (2013). Automating separation logic using SMT. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_54
[Submitted Version]
View
| Files available
| DOI
2013 | Conference Paper | IST-REx-ID: 2847 |
Bansal, K., Koskinen, E., Wies, T., & Zufferey, D. (2013). Structural Counter Abstraction. (N. Piterman & S. Smolka, Eds.). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy: Springer. https://doi.org/10.1007/978-3-642-36742-7_5
[Submitted Version]
View
| Files available
| DOI
| Download Submitted Version (ext.)
2012 | Conference Paper | IST-REx-ID: 3251 |
Zufferey, D., Wies, T., & Henzinger, T. A. (2012). Ideal abstractions for well structured transition systems (Vol. 7148, pp. 445–460). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. https://doi.org/10.1007/978-3-642-27940-9_29
[Submitted Version]
View
| Files available
| DOI
2011 | Conference Paper | IST-REx-ID: 3302 |
Henzinger, T. A., Singh, A., Singh, V., Wies, T., & Zufferey, D. (2011). Static scheduling in clouds (pp. 1–6). Presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, USENIX.
[Submitted Version]
View
| Files available
2011 | Conference Paper | IST-REx-ID: 3324 |
Piskac, R., & Wies, T. (2011). Decision procedures for automating termination proofs. In R. Jhala & D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA: Springer. https://doi.org/10.1007/978-3-642-18275-4_26
[Submitted Version]
View
| DOI
| Download Submitted Version (ext.)
2011 | Conference Paper | IST-REx-ID: 3358 |
Henzinger, T. A., Singh, V., Wies, T., & Zufferey, D. (2011). Scheduling large jobs by abstraction refinement (pp. 329–342). Presented at the EuroSys, Salzburg, Austria: ACM. https://doi.org/10.1145/1966445.1966476
[Published Version]
View
| DOI
| Download Published Version (ext.)
2011 | Technical Report | IST-REx-ID: 5383 |
Wies, T., Muñiz, M., & Kuncak, V. (2011). On an efficient decision procedure for imperative tree data structures. IST Austria. https://doi.org/10.15479/AT:IST-2011-0005
[Published Version]
View
| Files available
| DOI
2011 | Conference Paper | IST-REx-ID: 3323
Wies, T., Muñiz, M., & Kuncak, V. (2011). An efficient decision procedure for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the CADE 23: Automated Deduction , Wrocław, Poland: Springer. https://doi.org/10.1007/978-3-642-22438-6_36
View
| Files available
| DOI
2010 | Conference Paper | IST-REx-ID: 4364
Podelski, A., & Wies, T. (2010). Counterexample-guided focus (pp. 249–260). Presented at the POPL: Principles of Programming Languages, ACM. https://doi.org/10.1145/1707801.1706330
View
| DOI
2010 | Conference Paper | IST-REx-ID: 4378 |
Kuncak, V., Piskac, R., Suter, P., & Wies, T. (2010). Building a calculus of data structures. In G. Barthe & M. Hermenegildo (Eds.) (Vol. 5944, pp. 26–44). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Madrid, Spain: Springer. https://doi.org/10.1007/978-3-642-11319-2_6
[Submitted Version]
View
| DOI
| Download Submitted Version (ext.)
2010 | Conference Paper | IST-REx-ID: 4381 |
Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010). FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90). Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. https://doi.org/10.1109/CLOUD.2010.71
[Submitted Version]
View
| Files available
| DOI
2010 | Conference Paper | IST-REx-ID: 4380 |
Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010). A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded Software , Arizona, USA: ACM. https://doi.org/10.1145/1879021.1879022
[Submitted Version]
View
| Files available
| DOI
2010 | Journal Article | IST-REx-ID: 533
Hoenicke, J., Leino, K., Podelski, A., Schäf, M., & Wies, T. (2010). Doomed program points. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-010-0102-0
View
| DOI
2010 | Conference Paper | IST-REx-ID: 4361 |
Wies, T., Zufferey, D., & Henzinger, T. A. (2010). Forward analysis of depth-bounded processes. In L. Ong (Ed.) (Vol. 6014, pp. 94–108). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-12032-9_8
[Submitted Version]
View
| Files available
| DOI
2009 | Conference Paper | IST-REx-ID: 4365
Seghir, M., Podelski, A., & Wies, T. (2009). Abstraction Refinement for Quantified Array Assertions (pp. 3–18). Presented at the SAS: Static Analysis Symposium, Springer. https://doi.org/1556
View
| DOI
2009 | Conference Paper | IST-REx-ID: 4360
Wies, T., Piskac, R., & Kuncak, V. (2009). Combining Theories with Shared Set Operations (pp. 366–382). Presented at the FroCoS: Frontiers of Combining Systems, Springer. https://doi.org/1558
View
| DOI
2009 | Conference Paper | IST-REx-ID: 4375
Lahiri, S., Qadeer, S., Galeotti, J., Voung, J., & Wies, T. (2009). Intra-module Inference (pp. 493–508). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/1555
View
| DOI
2009 | Conference Paper | IST-REx-ID: 4377
Hoenicke, J., Leino, K. R., Podelski, A., Schäf, M., & Wies, T. (2009). It’s Doomed; We Can Prove It (pp. 338–353). Presented at the FM: Formal Methods, Springer. https://doi.org/1557
View
| DOI
2008 | Conference Paper | IST-REx-ID: 4366
Podelski, A., Rybalchenko, A., & Wies, T. (2008). Heap Assumptions on Demand (Vol. 5123, pp. 314–327). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-540-70545-1_31
View
| DOI
2007 | Conference Paper | IST-REx-ID: 4394
Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., & Rinard, M. (2007). Using First-Order Theorem Provers in the Jahob Data Structure Verification System (pp. 74–88). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Springer. https://doi.org/1552
View
| DOI
2007 | Conference Paper | IST-REx-ID: 4398
Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T., & Yang, H. (2007). Shape Analysis for Composite Data Structures (pp. 178–192). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/1553
View
| DOI
2006 | Conference Paper | IST-REx-ID: 4359
Wies, T., Kuncak, V., Lam, P., Podelski, A., & Rinard, M. (2006). Field Constraint Analysis (pp. 157–173). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Springer. https://doi.org/1551
View
| DOI
2005 | Conference Paper | IST-REx-ID: 4367
Podelski, A., & Wies, T. (2005). Boolean Heaps (pp. 267–282). Presented at the SAS: Static Analysis Symposium, Springer. https://doi.org/1550
View
| DOI
23 Publications
2013 | Conference Paper | IST-REx-ID: 2447 |
Piskac, R., Wies, T., & Zufferey, D. (2013). Automating separation logic using SMT. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_54
[Submitted Version]
View
| Files available
| DOI
2013 | Conference Paper | IST-REx-ID: 2847 |
Bansal, K., Koskinen, E., Wies, T., & Zufferey, D. (2013). Structural Counter Abstraction. (N. Piterman & S. Smolka, Eds.). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy: Springer. https://doi.org/10.1007/978-3-642-36742-7_5
[Submitted Version]
View
| Files available
| DOI
| Download Submitted Version (ext.)
2012 | Conference Paper | IST-REx-ID: 3251 |
Zufferey, D., Wies, T., & Henzinger, T. A. (2012). Ideal abstractions for well structured transition systems (Vol. 7148, pp. 445–460). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. https://doi.org/10.1007/978-3-642-27940-9_29
[Submitted Version]
View
| Files available
| DOI
2011 | Conference Paper | IST-REx-ID: 3302 |
Henzinger, T. A., Singh, A., Singh, V., Wies, T., & Zufferey, D. (2011). Static scheduling in clouds (pp. 1–6). Presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, USENIX.
[Submitted Version]
View
| Files available
2011 | Conference Paper | IST-REx-ID: 3324 |
Piskac, R., & Wies, T. (2011). Decision procedures for automating termination proofs. In R. Jhala & D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA: Springer. https://doi.org/10.1007/978-3-642-18275-4_26
[Submitted Version]
View
| DOI
| Download Submitted Version (ext.)
2011 | Conference Paper | IST-REx-ID: 3358 |
Henzinger, T. A., Singh, V., Wies, T., & Zufferey, D. (2011). Scheduling large jobs by abstraction refinement (pp. 329–342). Presented at the EuroSys, Salzburg, Austria: ACM. https://doi.org/10.1145/1966445.1966476
[Published Version]
View
| DOI
| Download Published Version (ext.)
2011 | Technical Report | IST-REx-ID: 5383 |
Wies, T., Muñiz, M., & Kuncak, V. (2011). On an efficient decision procedure for imperative tree data structures. IST Austria. https://doi.org/10.15479/AT:IST-2011-0005
[Published Version]
View
| Files available
| DOI
2011 | Conference Paper | IST-REx-ID: 3323
Wies, T., Muñiz, M., & Kuncak, V. (2011). An efficient decision procedure for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the CADE 23: Automated Deduction , Wrocław, Poland: Springer. https://doi.org/10.1007/978-3-642-22438-6_36
View
| Files available
| DOI
2010 | Conference Paper | IST-REx-ID: 4364
Podelski, A., & Wies, T. (2010). Counterexample-guided focus (pp. 249–260). Presented at the POPL: Principles of Programming Languages, ACM. https://doi.org/10.1145/1707801.1706330
View
| DOI
2010 | Conference Paper | IST-REx-ID: 4378 |
Kuncak, V., Piskac, R., Suter, P., & Wies, T. (2010). Building a calculus of data structures. In G. Barthe & M. Hermenegildo (Eds.) (Vol. 5944, pp. 26–44). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Madrid, Spain: Springer. https://doi.org/10.1007/978-3-642-11319-2_6
[Submitted Version]
View
| DOI
| Download Submitted Version (ext.)
2010 | Conference Paper | IST-REx-ID: 4381 |
Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010). FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90). Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. https://doi.org/10.1109/CLOUD.2010.71
[Submitted Version]
View
| Files available
| DOI
2010 | Conference Paper | IST-REx-ID: 4380 |
Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010). A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded Software , Arizona, USA: ACM. https://doi.org/10.1145/1879021.1879022
[Submitted Version]
View
| Files available
| DOI
2010 | Journal Article | IST-REx-ID: 533
Hoenicke, J., Leino, K., Podelski, A., Schäf, M., & Wies, T. (2010). Doomed program points. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-010-0102-0
View
| DOI
2010 | Conference Paper | IST-REx-ID: 4361 |
Wies, T., Zufferey, D., & Henzinger, T. A. (2010). Forward analysis of depth-bounded processes. In L. Ong (Ed.) (Vol. 6014, pp. 94–108). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-12032-9_8
[Submitted Version]
View
| Files available
| DOI
2009 | Conference Paper | IST-REx-ID: 4365
Seghir, M., Podelski, A., & Wies, T. (2009). Abstraction Refinement for Quantified Array Assertions (pp. 3–18). Presented at the SAS: Static Analysis Symposium, Springer. https://doi.org/1556
View
| DOI
2009 | Conference Paper | IST-REx-ID: 4360
Wies, T., Piskac, R., & Kuncak, V. (2009). Combining Theories with Shared Set Operations (pp. 366–382). Presented at the FroCoS: Frontiers of Combining Systems, Springer. https://doi.org/1558
View
| DOI
2009 | Conference Paper | IST-REx-ID: 4375
Lahiri, S., Qadeer, S., Galeotti, J., Voung, J., & Wies, T. (2009). Intra-module Inference (pp. 493–508). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/1555
View
| DOI
2009 | Conference Paper | IST-REx-ID: 4377
Hoenicke, J., Leino, K. R., Podelski, A., Schäf, M., & Wies, T. (2009). It’s Doomed; We Can Prove It (pp. 338–353). Presented at the FM: Formal Methods, Springer. https://doi.org/1557
View
| DOI
2008 | Conference Paper | IST-REx-ID: 4366
Podelski, A., Rybalchenko, A., & Wies, T. (2008). Heap Assumptions on Demand (Vol. 5123, pp. 314–327). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-540-70545-1_31
View
| DOI
2007 | Conference Paper | IST-REx-ID: 4394
Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., & Rinard, M. (2007). Using First-Order Theorem Provers in the Jahob Data Structure Verification System (pp. 74–88). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Springer. https://doi.org/1552
View
| DOI
2007 | Conference Paper | IST-REx-ID: 4398
Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T., & Yang, H. (2007). Shape Analysis for Composite Data Structures (pp. 178–192). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/1553
View
| DOI
2006 | Conference Paper | IST-REx-ID: 4359
Wies, T., Kuncak, V., Lam, P., Podelski, A., & Rinard, M. (2006). Field Constraint Analysis (pp. 157–173). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Springer. https://doi.org/1551
View
| DOI
2005 | Conference Paper | IST-REx-ID: 4367
Podelski, A., & Wies, T. (2005). Boolean Heaps (pp. 267–282). Presented at the SAS: Static Analysis Symposium, Springer. https://doi.org/1550
View
| DOI