Publications
See also my DBLP entry for a complete list of my publications.
In Conferences
-
VERMEER: A Tool for Tracing and Explaining Faulty C Programs
with Daniel Schwartz-Narbonne, Chanseok Oh, and Martin Schäf
To appear in Proceedings of ICSE, Demonstrations Track, 2015. -
Conflict-Directed Graph Coverage
with Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanović, and Philipp Rümmer
To appear in Proceedings of NFM, 2015. [pdf] -
Finding Minimum Type Error Sources
with Zvonimir Pavlinovic and Tim King
In Proceedings of OOPSLA, 2014. Best Paper Award. [pdf] -
Concolic Fault Abstraction
with Chanseok Oh, Martin Schäf, and Daniel Schwartz-Narbonne
In Proceedings of SCAM, 2014. [pdf] -
Automating
Separation Logic with Trees and Data with Ruzica
Piskac and Damien Zufferey
In Proceedings of CAV, 2014. [pdf] -
GRASShopper:
Complete Heap Verification with Mixed Specifications
with Ruzica Piskac and Damien
Zufferey
In Proceedings of TACAS, 2014. [pdf] -
Dynamic Package Interfaces
with Shahram Esmaeilsabzali, Rupak Majumdar, and Damien Zufferey
In Proceedings of FASE, 2014. [pdf] -
Cascade 2.0
with Wei Wang and Clark Barrett
In Proceedings of VMCAI, 2014. [pdf] -
Explaining Inconsistent Code
with Martin Schäf and Daniel Schwartz-Narbonne
In Proceedings of ESEC/FSE, 2013. [pdf] -
Automating Separation Logic using SMT
with Ruzica Piskac and Damien
Zufferey
In Proceedings of CAV, 2013. [pdf] [pdf-extended] -
Structural Counter Abstraction
with Kshitij Bansal, Eric Koskinen, and Damien
Zufferey
In Proceedings of TACAS, 2013. [pdf] [pdf-extended] -
Complete Instantiation-Based Interpolation
with Nishant Totla
In Proceedings of POPL, 2013. [pdf] [pdf-extended] -
Flow-Sensitive Fault Localization
with Jürgen Christ, Evren Ermis, and Martin
Schäf
In Proceedings of VMCAI, 2013. [pdf] -
Error Invariants
with Evren Ermis and Martin Schäf
In Proceedings of FM, 2012. [pdf] -
Ideal
Abstractions for Well-Structured Transition Systems
with Damien Zufferey and Thomas A. Henzinger
In Proceedings of VMCAI, 2012. [pdf] -
Deciding
Functional Lists with Sublist Sets
with Marco Muñiz and Viktor Kuncak
In Proceedings of VSTTE, 2012. [pdf] [pdf-extended] -
An Efficient Decision Procedure for Imperative Tree Data Structures
with Marco Muñiz and Viktor Kuncak
In Proceedings of CADE, 2011. [pdf] [pdf-extended] -
Scheduling Large Jobs by Abstraction Refinement with Thomas A. Henzinger, Vasu Singh, and Damien Zufferey
In Proceedings of EuroSys, 2011. [pdf] - Decision Procedures for Automating Termination Proofs with Ruzica Piskac
In Proceedings of VMCAI, 2011. [pdf] - A Marketplace for Cloud Resources with Thomas A. Henzinger, Vasu Singh, Anmol Tomar, and Damien Zufferey
In Proceedings of EMSOFT, 2010. [pdf] - FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment with Thomas A. Henzinger, Vasu Singh, Anmol Tomar, and Damien Zufferey
In Proceedings of IEEE CLOUD, 2010. [pdf] - Forward Analysis of Depth-Bounded Processes
with Damien Zufferey and Thomas A. Henzinger
In Proceedings of FoSSaCS, 2010. [pdf] - Counterexample-Guided Focus
with Andreas Podelski
In Proceedings of POPL, 2010. [pdf] [ppt-slides] -
Building a Calculus of Data Structures
with Viktor Kuncak, Ruzica Piskac, and Philippe Suter
In Proceedings of VMCAI, 2010. [pdf] - It's doomed; we can prove it
with Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, and Martin Schäf
In Proceedings of FM, 2009. [pdf] -
Combining Theories with Shared Set Operations
with Ruzica Piskac and Viktor Kuncak
In Proceedings of FroCoS, 2009. [pdf] [pdf-extended] [ppt-slides] -
Abstraction Refinement for Quantified Array Assertions
with Nassim Seghir and Andreas Podelski
In Proceedings of SAS, 2009. [pdf] -
Intra-module Inference
with Shuvendu Lahiri, Shaz Qadeer, Juan Galeotti, and Jan Voung
In Proceedings of CAV, 2009. [pdf] -
Heap Assumptions on Demand
with Andreas Podelski and Andrey Rybalchenko
In Proceedings of CAV, 2008. [pdf] [pdf-extended] -
Shape analysis for composite data structures
with Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, and Hongseok Yang
In Proceedings of CAV, 2007. [pdf] -
Using First-Order Theorem Provers in the Jahob Data Structure Verification System
with Charles Bouillaguet, Viktor Kuncak, Karen Zee, and Martin Rinard
In Proceedings of VMCAI, 2007. [pdf] -
Field Constraint Analysis
with Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard
In Proceedings of VMCAI, 2006. [pdf] [pdf-extended] [pdf-slides] -
Boolean Heaps
with Andreas Podelski
In Proceedings of SAS, 2005. [pdf] [pdf-slides]
In Journals
- Preface - Invariant Generation with Gudmund Grov
Science of Computer Programming (SCICO). 93, 2014. - Doomed Program Points with Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, and Martin Schäf
Formal Methods in System Design (FMSD). 37(2):171, 2010. [pdf]
In Workshops
-
Static
Scheduling in Clouds
with Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, and Damien Zufferey
In Proceedings of HotCloud, 2011. [pdf] - (EC)2 in EC2 with Thomas A. Henzinger, Vasu Singh, Anmol Tomar, and Damien Zufferey
(EC)2 Workshop, 2010. [pdf] -
Verifying Complex Properties using Symbolic Shape Analysis
with Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard
Workshop on Heap Abstraction and Verification, March 2007. [pdf]
Thesis
-
Symbolic Shape Analysis
PhD Thesis, University of Freiburg, Freiburg, Germany, 2009. [pdf]
Technical Reports
-
Automating Separation Logic using SMT
with Ruzica Piskac and Damien Zufferey
NYU Technical Report TR2013-954, March, 2013. [pdf] -
Complete Instantiation-Based Interpolation
with Nishant Totla
NYU Technical Report TR2012-950, July, 2012. [pdf] -
Structural Counter Abstraction
with Kshitij Bansal, Eric Koskinen, and Damien Zufferey
NYU Technical Report TR2012-947, April, 2012. [pdf] -
On an Efficient Decision Procedure for Imperative Tree Data Structures
with Marco Muñiz and Viktor Kuncak
IST Technical Report IST-2011-0005, April, 2011. [pdf] -
On Deciding Functional Lists with Sublist Sets
with Marco Muñiz and Viktor Kuncak
EPFL Technical Report EPFL-REPORT-148361, April, 2010. [pdf] -
On Combining Theories with Shared Set Operations
with Ruzica Piskac and Viktor Kuncak
EPFL Technical Report LARA-REPORT-2009-002. February, 2009. [pdf] -
On Set-Driven Combination of Logics and Verifiers
with Viktor Kuncak
EPFL Technical Report LARA-REPORT-2009-001. 2009. [pdf] - On
Verifying Complex Properties using Symbolic Shape Analysis
with Viktor Kuncak, Karen Zee,
Andreas Podelski, and Martin Rinard
Max-Planck Institute for Computer Science Technical Report MPI-I-2006-2-1. 2006 [pdf] - On Field
Constraint Analysis with Viktor Kuncak, Patrick Lam,
Andreas Podelski, and Martin Rinard
MIT CSAIL Technical Report MIT-CSAIL-TR-2005-072, MIT-LCS-TR-1010. 2005. [pdf]