| 2015 | APLAS | Bottom-Up Context-Sensitive Pointer Analysis for Java. | Yu Feng, Xinyu Wang, Isil Dillig, Thomas Dillig |
| 2014 | CAV | Optimal Guard Synthesis for Memory Safety. | Thomas Dillig, Isil Dillig, Swarat Chaudhuri |
| 2014 | PLDI | Consolidation of queries with user-defined functions. | Marcelo Sousa, Isil Dillig, Dimitrios Vytiniotis, Thomas Dillig, Christos Gkantsidis |
| 2013 | APLAS | Automated Inference of Library Specifications for Source-Sink Property Verification. | Haiyan Zhu, Thomas Dillig, Isil Dillig |
| 2013 | CAV | Explain: A Tool for Performing Abductive Inference. | Isil Dillig, Thomas Dillig |
| 2013 | OOPSLA | Inductive invariant generation via abductive inference. | Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan |
| 2013 | TACAS | Synthesis of Circular Compositional Program Proofs via Abduction. | Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv |
| 2012 | CAV | Minimum Satisfying Assignments for SMT. | Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Alex Aiken |
| 2012 | PLDI | Automated error diagnosis using abductive inference. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2011 | CAV | Simplifying Loop Invariant Generation Using Splitter Predicates. | Rahul Sharma, Isil Dillig, Thomas Dillig, Alex Aiken |
| 2011 | PLDI | Precise and compact modular procedure summaries for heap manipulating programs. | Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv |
| 2011 | POPL | Precise reasoning for programs using containers. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2010 | ESOP | Fluid Updates: Beyond Strong vs. Weak Updates. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2010 | OOPSLA | Symbolic heap abstraction with demand-driven axiomatization of memory invariants. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2010 | SAS | Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2009 | CAV | Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2008 | PLDI | Sound, complete and scalable path-sensitive analysis. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2007 | PLDI | Static error detection using semantic inconsistency inference. | Isil Dillig, Thomas Dillig, Alex Aiken |