Thomas Wies
Henzinger_Thomas Group
23 Publications
2013 | Published | Conference Paper | IST-REx-ID: 2447 |

Piskac, Ruzica, et al. Automating Separation Logic Using SMT. Vol. 8044, Springer, 2013, pp. 773–89, doi:10.1007/978-3-642-39799-8_54.
[Submitted Version]
View
| Files available
| DOI
2013 | Published | Conference Paper | IST-REx-ID: 2847 |

Bansal, Kshitij, et al. Structural Counter Abstraction. Edited by Nir Piterman and Scott Smolka, vol. 7795, Springer, 2013, pp. 62–77, doi:10.1007/978-3-642-36742-7_5.
[Submitted Version]
View
| Files available
| DOI
| Download Submitted Version (ext.)
2012 | Published | Conference Paper | IST-REx-ID: 3251 |

Zufferey, Damien, et al. Ideal Abstractions for Well Structured Transition Systems. Vol. 7148, Springer, 2012, pp. 445–60, doi:10.1007/978-3-642-27940-9_29.
[Submitted Version]
View
| Files available
| DOI
2011 | Published | Technical Report | IST-REx-ID: 5383 |

Wies, Thomas, et al. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria, 2011, doi:10.15479/AT:IST-2011-0005.
[Published Version]
View
| Files available
| DOI
2011 | Published | Conference Paper | IST-REx-ID: 3302 |

Henzinger, Thomas A., et al. Static Scheduling in Clouds. USENIX, 2011, pp. 1–6.
[Submitted Version]
View
| Files available
2011 | Published | Conference Paper | IST-REx-ID: 3323
Wies, Thomas, et al. An Efficient Decision Procedure for Imperative Tree Data Structures. Vol. 6803, Springer, 2011, pp. 476–91, doi:10.1007/978-3-642-22438-6_36.
View
| Files available
| DOI
2011 | Published | Conference Paper | IST-REx-ID: 3324 |

Piskac, Ruzica, and Thomas Wies. Decision Procedures for Automating Termination Proofs. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011, pp. 371–86, doi:10.1007/978-3-642-18275-4_26.
[Submitted Version]
View
| DOI
| Download Submitted Version (ext.)
2011 | Published | Conference Paper | IST-REx-ID: 3358 |

Henzinger, Thomas A., et al. Scheduling Large Jobs by Abstraction Refinement. ACM, 2011, pp. 329–42, doi:10.1145/1966445.1966476.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2010 | Published | Conference Paper | IST-REx-ID: 4364
Podelski, Andreas, and Thomas Wies. Counterexample-Guided Focus. ACM, 2010, pp. 249–60, doi:10.1145/1707801.1706330.
View
| DOI
2010 | Published | Conference Paper | IST-REx-ID: 4378 |

Kuncak, Viktor, et al. Building a Calculus of Data Structures. Edited by Gilles Barthe and Manuel Hermenegildo, vol. 5944, Springer, 2010, pp. 26–44, doi:10.1007/978-3-642-11319-2_6.
[Submitted Version]
View
| DOI
| Download Submitted Version (ext.)
2010 | Published | Conference Paper | IST-REx-ID: 4380 |

Henzinger, Thomas A., et al. A Marketplace for Cloud Resources. ACM, 2010, pp. 1–8, doi:10.1145/1879021.1879022.
[Submitted Version]
View
| Files available
| DOI
2010 | Published | Conference Paper | IST-REx-ID: 4381 |

Henzinger, Thomas A., et al. FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment. IEEE, 2010, pp. 83–90, doi:10.1109/CLOUD.2010.71.
[Submitted Version]
View
| Files available
| DOI
2010 | Published | Journal Article | IST-REx-ID: 533
Hoenicke, Jochen, et al. “Doomed Program Points.” Formal Methods in System Design, vol. 37, no. 2–3, Springer, 2010, pp. 171–99, doi:10.1007/s10703-010-0102-0.
View
| DOI
2010 | Published | Conference Paper | IST-REx-ID: 4361 |

Wies, Thomas, et al. Forward Analysis of Depth-Bounded Processes. Edited by Luke Ong, vol. 6014, Springer, 2010, pp. 94–108, doi:10.1007/978-3-642-12032-9_8.
[Submitted Version]
View
| Files available
| DOI
2009 | Published | Conference Paper | IST-REx-ID: 4360
Wies, Thomas, et al. “Combining Theories with Shared Set Operations.” 7th International Symposium on Frontiers of Combining Systems, vol. 5749, Springer, 2009, pp. 366–82, doi:10.1007/978-3-642-04222-5_23.
View
| DOI
2009 | Published | Conference Paper | IST-REx-ID: 4377
Hoenicke, Jochen, et al. “It’s Doomed; We Can Prove It.” Second World Congress on Formal Methods, vol. 5850, Springer, 2009, pp. 338–53, doi:10.1007/978-3-642-05089-3_22.
View
| DOI
2009 | Published | Conference Paper | IST-REx-ID: 4365
Seghir, Mohamed, et al. “Abstraction Refinement for Quantified Array Assertions.” 16th International Symposium on Static Analysis, vol. 5673, Springer, 2009, pp. 3–18, doi:10.1007/978-3-642-03237-0_3.
View
| DOI
2009 | Published | Conference Paper | IST-REx-ID: 4375
Lahiri, Shuvendu, et al. “Intra-Module Inference.” 21st International Conference on Computer Aided Verification, vol. 5643, Springer, 2009, pp. 493–508, doi:10.1007/978-3-642-02658-4_37.
View
| DOI
2008 | Published | Conference Paper | IST-REx-ID: 4366
Podelski, Andreas, et al. Heap Assumptions on Demand. Vol. 5123, Springer, 2008, pp. 314–27, doi:10.1007/978-3-540-70545-1_31.
View
| DOI
2007 | Published | Conference Paper | IST-REx-ID: 4394
Bouillaguet, Charles, et al. “Using First-Order Theorem Provers in the Jahob Data Structure Verification System.” 8th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 4349, Springer, 2007, pp. 74–88, doi:10.1007/978-3-540-69738-1_5.
View
| DOI
2007 | Published | Conference Paper | IST-REx-ID: 4398
Berdine, Josh, et al. “Shape Analysis for Composite Data Structures.” 19th International Conference on Computer Aided Verification, vol. 4590, Springer, 2007, pp. 178–92, doi:10.1007/978-3-540-73368-3_22.
View
| DOI
2006 | Published | Conference Paper | IST-REx-ID: 4359
Wies, Thomas, et al. “Field Constraint Analysis.” 7th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 3855, Springer, 2006, pp. 157–73, doi:10.1007/11609773_11.
View
| DOI
2005 | Published | Conference Paper | IST-REx-ID: 4367
Podelski, Andreas, and Thomas Wies. “Boolean Heaps.” 12th International Symposium on Static Analysis, vol. 3672, Springer, 2005, pp. 268–83, doi:10.1007/11547662_19.
View
| DOI
Grants
23 Publications
2013 | Published | Conference Paper | IST-REx-ID: 2447 |

Piskac, Ruzica, et al. Automating Separation Logic Using SMT. Vol. 8044, Springer, 2013, pp. 773–89, doi:10.1007/978-3-642-39799-8_54.
[Submitted Version]
View
| Files available
| DOI
2013 | Published | Conference Paper | IST-REx-ID: 2847 |

Bansal, Kshitij, et al. Structural Counter Abstraction. Edited by Nir Piterman and Scott Smolka, vol. 7795, Springer, 2013, pp. 62–77, doi:10.1007/978-3-642-36742-7_5.
[Submitted Version]
View
| Files available
| DOI
| Download Submitted Version (ext.)
2012 | Published | Conference Paper | IST-REx-ID: 3251 |

Zufferey, Damien, et al. Ideal Abstractions for Well Structured Transition Systems. Vol. 7148, Springer, 2012, pp. 445–60, doi:10.1007/978-3-642-27940-9_29.
[Submitted Version]
View
| Files available
| DOI
2011 | Published | Technical Report | IST-REx-ID: 5383 |

Wies, Thomas, et al. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria, 2011, doi:10.15479/AT:IST-2011-0005.
[Published Version]
View
| Files available
| DOI
2011 | Published | Conference Paper | IST-REx-ID: 3302 |

Henzinger, Thomas A., et al. Static Scheduling in Clouds. USENIX, 2011, pp. 1–6.
[Submitted Version]
View
| Files available
2011 | Published | Conference Paper | IST-REx-ID: 3323
Wies, Thomas, et al. An Efficient Decision Procedure for Imperative Tree Data Structures. Vol. 6803, Springer, 2011, pp. 476–91, doi:10.1007/978-3-642-22438-6_36.
View
| Files available
| DOI
2011 | Published | Conference Paper | IST-REx-ID: 3324 |

Piskac, Ruzica, and Thomas Wies. Decision Procedures for Automating Termination Proofs. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011, pp. 371–86, doi:10.1007/978-3-642-18275-4_26.
[Submitted Version]
View
| DOI
| Download Submitted Version (ext.)
2011 | Published | Conference Paper | IST-REx-ID: 3358 |

Henzinger, Thomas A., et al. Scheduling Large Jobs by Abstraction Refinement. ACM, 2011, pp. 329–42, doi:10.1145/1966445.1966476.
[Published Version]
View
| DOI
| Download Published Version (ext.)
2010 | Published | Conference Paper | IST-REx-ID: 4364
Podelski, Andreas, and Thomas Wies. Counterexample-Guided Focus. ACM, 2010, pp. 249–60, doi:10.1145/1707801.1706330.
View
| DOI
2010 | Published | Conference Paper | IST-REx-ID: 4378 |

Kuncak, Viktor, et al. Building a Calculus of Data Structures. Edited by Gilles Barthe and Manuel Hermenegildo, vol. 5944, Springer, 2010, pp. 26–44, doi:10.1007/978-3-642-11319-2_6.
[Submitted Version]
View
| DOI
| Download Submitted Version (ext.)
2010 | Published | Conference Paper | IST-REx-ID: 4380 |

Henzinger, Thomas A., et al. A Marketplace for Cloud Resources. ACM, 2010, pp. 1–8, doi:10.1145/1879021.1879022.
[Submitted Version]
View
| Files available
| DOI
2010 | Published | Conference Paper | IST-REx-ID: 4381 |

Henzinger, Thomas A., et al. FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment. IEEE, 2010, pp. 83–90, doi:10.1109/CLOUD.2010.71.
[Submitted Version]
View
| Files available
| DOI
2010 | Published | Journal Article | IST-REx-ID: 533
Hoenicke, Jochen, et al. “Doomed Program Points.” Formal Methods in System Design, vol. 37, no. 2–3, Springer, 2010, pp. 171–99, doi:10.1007/s10703-010-0102-0.
View
| DOI
2010 | Published | Conference Paper | IST-REx-ID: 4361 |

Wies, Thomas, et al. Forward Analysis of Depth-Bounded Processes. Edited by Luke Ong, vol. 6014, Springer, 2010, pp. 94–108, doi:10.1007/978-3-642-12032-9_8.
[Submitted Version]
View
| Files available
| DOI
2009 | Published | Conference Paper | IST-REx-ID: 4360
Wies, Thomas, et al. “Combining Theories with Shared Set Operations.” 7th International Symposium on Frontiers of Combining Systems, vol. 5749, Springer, 2009, pp. 366–82, doi:10.1007/978-3-642-04222-5_23.
View
| DOI
2009 | Published | Conference Paper | IST-REx-ID: 4377
Hoenicke, Jochen, et al. “It’s Doomed; We Can Prove It.” Second World Congress on Formal Methods, vol. 5850, Springer, 2009, pp. 338–53, doi:10.1007/978-3-642-05089-3_22.
View
| DOI
2009 | Published | Conference Paper | IST-REx-ID: 4365
Seghir, Mohamed, et al. “Abstraction Refinement for Quantified Array Assertions.” 16th International Symposium on Static Analysis, vol. 5673, Springer, 2009, pp. 3–18, doi:10.1007/978-3-642-03237-0_3.
View
| DOI
2009 | Published | Conference Paper | IST-REx-ID: 4375
Lahiri, Shuvendu, et al. “Intra-Module Inference.” 21st International Conference on Computer Aided Verification, vol. 5643, Springer, 2009, pp. 493–508, doi:10.1007/978-3-642-02658-4_37.
View
| DOI
2008 | Published | Conference Paper | IST-REx-ID: 4366
Podelski, Andreas, et al. Heap Assumptions on Demand. Vol. 5123, Springer, 2008, pp. 314–27, doi:10.1007/978-3-540-70545-1_31.
View
| DOI
2007 | Published | Conference Paper | IST-REx-ID: 4394
Bouillaguet, Charles, et al. “Using First-Order Theorem Provers in the Jahob Data Structure Verification System.” 8th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 4349, Springer, 2007, pp. 74–88, doi:10.1007/978-3-540-69738-1_5.
View
| DOI
2007 | Published | Conference Paper | IST-REx-ID: 4398
Berdine, Josh, et al. “Shape Analysis for Composite Data Structures.” 19th International Conference on Computer Aided Verification, vol. 4590, Springer, 2007, pp. 178–92, doi:10.1007/978-3-540-73368-3_22.
View
| DOI
2006 | Published | Conference Paper | IST-REx-ID: 4359
Wies, Thomas, et al. “Field Constraint Analysis.” 7th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 3855, Springer, 2006, pp. 157–73, doi:10.1007/11609773_11.
View
| DOI
2005 | Published | Conference Paper | IST-REx-ID: 4367
Podelski, Andreas, and Thomas Wies. “Boolean Heaps.” 12th International Symposium on Static Analysis, vol. 3672, Springer, 2005, pp. 268–83, doi:10.1007/11547662_19.
View
| DOI