ISTA Research Explorer

Thomas Wies

Henzinger_Thomas Group

23 Publications

Mark all

[23]

2013 | Published | Conference Paper | IST-REx-ID: 2447 |

Piskac R, Wies T, Zufferey D. 2013. Automating separation logic using SMT. 8044, 773–789.

[Submitted Version] View | Files available | DOI

[22]

2013 | Published | Conference Paper | IST-REx-ID: 2847 |

Bansal K, Koskinen E, Wies T, Zufferey D. 2013. Structural Counter Abstraction (eds. N. Piterman & S. Smolka). 7795, 62–77.

[Submitted Version] View | Files available | DOI | Download Submitted Version (ext.)

[21]

2012 | Published | Conference Paper | IST-REx-ID: 3251 |

Zufferey D, Wies T, Henzinger TA. 2012. Ideal abstractions for well structured transition systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 445–460.

[Submitted Version] View | Files available | DOI

[20]

2011 | Published | 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, 25p.

[Published Version] View | Files available | DOI

[19]

2011 | Published | Conference Paper | IST-REx-ID: 3302 |

Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling in clouds. HotCloud: Workshop on Hot Topics in Cloud Computing, 1–6.

[Submitted Version] View | Files available

[18]

2011 | Published | Conference Paper | IST-REx-ID: 3323

Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491.

View | Files available | DOI

[17]

2011 | Published | Conference Paper | IST-REx-ID: 3324 |

Piskac R, Wies T. 2011. Decision procedures for automating termination proofs. VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538, 371–386.

[Submitted Version] View | DOI | Download Submitted Version (ext.)

[16]

2011 | Published | Conference Paper | IST-REx-ID: 3358 |

Henzinger TA, Singh V, Wies T, Zufferey D. 2011. Scheduling large jobs by abstraction refinement. EuroSys, 329–342.

[Published Version] View | DOI | Download Published Version (ext.)

[15]

2010 | Published | Conference Paper | IST-REx-ID: 4364

Podelski A, Wies T. 2010. Counterexample-guided focus. POPL: Principles of Programming Languages, 249–260.

View | DOI

[14]

2010 | Published | Conference Paper | IST-REx-ID: 4378 |

Kuncak V, Piskac R, Suter P, Wies T. 2010. Building a calculus of data structures. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 5944, 26–44.

[Submitted Version] View | DOI | Download Submitted Version (ext.)

[13]

2010 | Published | Conference Paper | IST-REx-ID: 4380 |

Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for cloud resources. EMSOFT: Embedded Software , 1–8.

[Submitted Version] View | Files available | DOI

[12]

2010 | Published | Conference Paper | IST-REx-ID: 4381 |

Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90.

[Submitted Version] View | Files available | DOI

[11]

2010 | Published | 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. 37(2–3), 171–199.

View | DOI

[10]

2010 | Published | Conference Paper | IST-REx-ID: 4361 |

Wies T, Zufferey D, Henzinger TA. 2010. Forward analysis of depth-bounded processes. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 6014, 94–108.

[Submitted Version] View | Files available | DOI

[9]

2009 | Published | Conference Paper | IST-REx-ID: 4360

Wies T, Piskac R, Kuncak V. 2009. Combining Theories with Shared Set Operations. FroCoS: Frontiers of Combining Systems, LNCS 5749, , 366–382.

View | DOI

[8]

2009 | Published | Conference Paper | IST-REx-ID: 4365

Seghir M, Podelski A, Wies T. 2009. Abstraction Refinement for Quantified Array Assertions. SAS: Static Analysis Symposium, LNCS 5673, , 3–18.

View | DOI

[7]

2009 | Published | Conference Paper | IST-REx-ID: 4375

Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. 2009. Intra-module Inference. CAV: Computer Aided Verification, LNCS 5643, , 493–508.

View | DOI

[6]

2009 | Published | Conference Paper | IST-REx-ID: 4377

Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. 2009. It’s Doomed; We Can Prove It. FM: Formal Methods, LNCS 5850, , 338–353.

View | DOI

[5]

2008 | Published | Conference Paper | IST-REx-ID: 4366

Podelski A, Rybalchenko A, Wies T. 2008. Heap Assumptions on Demand. CAV: Computer Aided Verification, LNCS, vol. 5123, 314–327.

View | DOI

[4]

2007 | Published | 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. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS 4349, , 74–88.

View | DOI

[3]

2007 | Published | 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. CAV: Computer Aided Verification, LNCS 4590, , 178–192.

View | DOI

[2]

2006 | Published | Conference Paper | IST-REx-ID: 4359

Wies T, Kuncak V, Lam P, Podelski A, Rinard M. 2006. Field Constraint Analysis. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS 3855, , 157–173.

View | DOI

[1]

2005 | Published | Conference Paper | IST-REx-ID: 4367

Podelski A, Wies T. 2005. Boolean Heaps. SAS: Static Analysis Symposium, LNCS 3672, , 267–282.

View | DOI

Grants

23 Publications

Mark all

[23]

2013 | Published | Conference Paper | IST-REx-ID: 2447 |

Piskac R, Wies T, Zufferey D. 2013. Automating separation logic using SMT. 8044, 773–789.

[Submitted Version] View | Files available | DOI

[22]

2013 | Published | Conference Paper | IST-REx-ID: 2847 |

Bansal K, Koskinen E, Wies T, Zufferey D. 2013. Structural Counter Abstraction (eds. N. Piterman & S. Smolka). 7795, 62–77.

[Submitted Version] View | Files available | DOI | Download Submitted Version (ext.)

[21]

2012 | Published | Conference Paper | IST-REx-ID: 3251 |

Zufferey D, Wies T, Henzinger TA. 2012. Ideal abstractions for well structured transition systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 445–460.

[Submitted Version] View | Files available | DOI

[20]

2011 | Published | 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, 25p.

[Published Version] View | Files available | DOI

[19]

2011 | Published | Conference Paper | IST-REx-ID: 3302 |

Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling in clouds. HotCloud: Workshop on Hot Topics in Cloud Computing, 1–6.

[Submitted Version] View | Files available

[18]

2011 | Published | Conference Paper | IST-REx-ID: 3323

Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491.

View | Files available | DOI

[17]

2011 | Published | Conference Paper | IST-REx-ID: 3324 |

Piskac R, Wies T. 2011. Decision procedures for automating termination proofs. VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538, 371–386.

[Submitted Version] View | DOI | Download Submitted Version (ext.)

[16]

2011 | Published | Conference Paper | IST-REx-ID: 3358 |

Henzinger TA, Singh V, Wies T, Zufferey D. 2011. Scheduling large jobs by abstraction refinement. EuroSys, 329–342.

[Published Version] View | DOI | Download Published Version (ext.)

[15]

2010 | Published | Conference Paper | IST-REx-ID: 4364

Podelski A, Wies T. 2010. Counterexample-guided focus. POPL: Principles of Programming Languages, 249–260.

View | DOI

[14]

2010 | Published | Conference Paper | IST-REx-ID: 4378 |

Kuncak V, Piskac R, Suter P, Wies T. 2010. Building a calculus of data structures. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 5944, 26–44.

[Submitted Version] View | DOI | Download Submitted Version (ext.)

[13]

2010 | Published | Conference Paper | IST-REx-ID: 4380 |

Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for cloud resources. EMSOFT: Embedded Software , 1–8.

[Submitted Version] View | Files available | DOI

[12]

2010 | Published | Conference Paper | IST-REx-ID: 4381 |

Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90.

[Submitted Version] View | Files available | DOI

[11]

2010 | Published | 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. 37(2–3), 171–199.

View | DOI

[10]

2010 | Published | Conference Paper | IST-REx-ID: 4361 |

Wies T, Zufferey D, Henzinger TA. 2010. Forward analysis of depth-bounded processes. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 6014, 94–108.

[Submitted Version] View | Files available | DOI

[9]

2009 | Published | Conference Paper | IST-REx-ID: 4360

Wies T, Piskac R, Kuncak V. 2009. Combining Theories with Shared Set Operations. FroCoS: Frontiers of Combining Systems, LNCS 5749, , 366–382.

View | DOI

[8]

2009 | Published | Conference Paper | IST-REx-ID: 4365

Seghir M, Podelski A, Wies T. 2009. Abstraction Refinement for Quantified Array Assertions. SAS: Static Analysis Symposium, LNCS 5673, , 3–18.

View | DOI

[7]

2009 | Published | Conference Paper | IST-REx-ID: 4375

Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. 2009. Intra-module Inference. CAV: Computer Aided Verification, LNCS 5643, , 493–508.

View | DOI

[6]

2009 | Published | Conference Paper | IST-REx-ID: 4377

Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. 2009. It’s Doomed; We Can Prove It. FM: Formal Methods, LNCS 5850, , 338–353.

View | DOI

[5]

2008 | Published | Conference Paper | IST-REx-ID: 4366

Podelski A, Rybalchenko A, Wies T. 2008. Heap Assumptions on Demand. CAV: Computer Aided Verification, LNCS, vol. 5123, 314–327.

View | DOI

[4]

2007 | Published | Conference Paper | IST-REx-ID: 4394

View | DOI

[3]

2007 | Published | 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. CAV: Computer Aided Verification, LNCS 4590, , 178–192.

View | DOI

[2]

2006 | Published | Conference Paper | IST-REx-ID: 4359

Wies T, Kuncak V, Lam P, Podelski A, Rinard M. 2006. Field Constraint Analysis. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS 3855, , 157–173.

View | DOI

[1]

2005 | Published | Conference Paper | IST-REx-ID: 4367

Podelski A, Wies T. 2005. Boolean Heaps. SAS: Static Analysis Symposium, LNCS 3672, , 267–282.

View | DOI

Thomas Wies

23 Publications

Search

Filter Publications

Display / Sort

Export / Embed

Grants

23 Publications

Search

Filter Publications

Display / Sort

Export / Embed

Thomas Wies

23 Publications

Search

Filter Publications

Display / Sort

Export / Embed

Export Options

Grants

23 Publications

Search

Filter Publications

Display / Sort

Export / Embed

Export Options