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.

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.

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.

Henzinger, Thomas A., et al. Static Scheduling in Clouds. USENIX, 2011, pp. 1–6.

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.

Henzinger, Thomas A., et al. Scheduling Large Jobs by Abstraction Refinement. ACM, 2011, pp. 329–42, doi:10.1145/1966445.1966476.

Wies, Thomas, et al. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria, 2011, doi:10.15479/AT:IST-2011-0005.

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.

Podelski, Andreas, and Thomas Wies. Counterexample-Guided Focus. ACM, 2010, pp. 249–60, doi:10.1145/1707801.1706330.

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.

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.

Henzinger, Thomas A., et al. A Marketplace for Cloud Resources. ACM, 2010, pp. 1–8, doi:10.1145/1879021.1879022.

Hoenicke, Jochen, et al. “Doomed Program Points.”10.1007/s10703-010-0102-0__Formal Methods in System Design, vol. 37, no. 2–3, Springer, 2010, pp. 171–99, doi:10.1007/s10703-010-0102-0.

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.

Seghir, Mohamed, et al. Abstraction Refinement for Quantified Array Assertions. Springer, 2009, pp. 3–18, doi:1556.

Wies, Thomas, et al. Combining Theories with Shared Set Operations. Springer, 2009, pp. 366–82, doi:1558.

Lahiri, Shuvendu, et al. Intra-Module Inference. Springer, 2009, pp. 493–508, doi:1555.

Hoenicke, Jochen, et al. It’s Doomed; We Can Prove It. Springer, 2009, pp. 338–53, doi:1557.

Podelski, Andreas, et al. Heap Assumptions on Demand. Vol. 5123, Springer, 2008, pp. 314–27, doi:10.1007/978-3-540-70545-1_31.

Bouillaguet, Charles, et al. Using First-Order Theorem Provers in the Jahob Data Structure Verification System. Springer, 2007, pp. 74–88, doi:1552.

Berdine, Josh, et al. Shape Analysis for Composite Data Structures. Springer, 2007, pp. 178–92, doi:1553.

Wies, Thomas, et al. Field Constraint Analysis. Springer, 2006, pp. 157–73, doi:1551.

Podelski, Andreas, and Thomas Wies. Boolean Heaps. Springer, 2005, pp. 267–82, doi:1550.