|
Thomas Dillig
Adjunct Professor
Computer Science
UT Austin
|
E-mail: tdillig@cs.utexas.edu
I have moved full time to BIG, am expert firm specializing in Consulting and Custom Technology that I co-founded.
My main research interests are program verification and constraint solving. I have worked on precise, scalable and modular analysis of unbounded data structures, such as arrays and containers. My work on constraint solving focuses on online constraint simplification as well as integer linear programming.
- SQLizer: Query Synthesis from Natural Language . Navid Yaghmazadeh, Yuepeng Wang, Isil Dillig, Thomas Dillig. In OOPSLA'17. (Distinguished paper award)
- Bottom-up Context-Sensitive Pointer Analysis for Java. Yu Feng, Xinyu Wang, Isil Dillig, Thomas Dillig. In APLAS 2015.
- Optimal Guard Synthesis for Memory Safety.
Thomas Dillig, Isil Dillig, Swarat Chaudhuri. CAV 2014. [Extended version]
[slides]
- Consolidation of Queries with User-Defined Functions .
Marcelo Sousa, Isil Dillig, Dimitrios Vytionitis, Thomas Dillig, Christos Gkantsidis. PLDI 2014.
- Automated Inference of Library Specifications for Source-Sink Property Verification.
Haiyan Zhu, Thomas Dillig, Isil Dillig. APLAS 2013.
- Inductive Invariant Generation via Abductive Inference .
Isil Dillig, Thomas Dillig, Boyang Li, Ken McMillan. OOPSLA 2013.
- EXPLAIN: A Tool for Performing Abductive Inference .
Isil Dillig, Thomas Dillig. CAV 2013.
- Synthesis of Circular Compositional Program Proofs via Abduction .
Boyang Li, Isil Dillig, Thomas Dillig, Ken McMillan, Mooly Sagiv. TACAS 2013.
- Minimum Satisfying Assignments for SMT. Isil Dillig, Thomas Dillig, Ken McMillan, Alex Aiken.
Computer Aided Verification (CAV) 2012.
- Automated Error Diagnosis Using Abductive Inference. Isil Dillig, Thomas Dillig, Alex Aiken.
In Programming Languages Design and Implementation (PLDI) 2012. [Extended version]
- Simplifying Loop Invariant Generation Using Splitter Predicates
Rahul Sharma, Isil Dillig, Thomas Dillig, Alex Aiken. Proceedings of the International Conference on Computer Aided Verification (CAV) 2011.
- Precise and Compact Modular Procedure Summaries for Heap
Manipulating Programs
Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv. Programming Language Design and
Implementation (PLDI) 2011.
- Precise Reasoning for Programs Using Containers
Isil Dillig, Thomas Dillig, Alex Aiken. Principles of Programming Languages (POPL) 2011. Austin, TX.
- Symbolic Heap Abstraction with Demand-Driven Axiomatization of Memory Invariants
Isil Dillig, Thomas Dillig, Alex Aiken. Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2010.
- Small Formulas for Large Programs: On-line Constraint Simplification in Scalable Static Analysis
Isil Dillig, Thomas Dillig, Alex Aiken. Static Analysis Symposium (SAS) 2010. Perpignan, France.
- Reasoning About the Unknown in Static Analysis
Isil Dillig, Thomas Dillig, Alex Aiken. Research highlight, Communications of the ACM (CACM), August 2010.
- Fluid Updates: Beyond Strong vs. Weak Updates
Isil Dillig, Thomas Dillig, Alex Aiken. Proceedings of the European
Symposium on Programming (ESOP) 2010. Paphos, Cyprus. (Conference version without appendix)
- Cuts from Proofs: A
Complete and Practical Technique for Solving Linear Inequalities over Integers
Isil Dillig, Thomas Dillig, Alex Aiken. Proceedings of
Computer Aided Verification (CAV) 2009. Grenoble, France.
- SAIL: Static Analysis Intermediate Language with a Two-Level Representation
Isil Dillig, Thomas Dillig, Alex Aiken. Technical Report, Stanford University 2009.
[Project Website]
- Sound, Complete, and
Scalable Path-Sensitive Analysis
Isil Dillig, Thomas Dillig, Alex
Aiken. Proceedings of the Conference on Programming Language Design and
Implementation (PLDI), June 2008. Tucson, AZ.
- The CLOSER:
Automating Resource Management in Java
Isil Dillig, Thomas Dillig,
Eran Yahav, Satish Chandra. Proceedings of the International Symposium on Memory
Management (ISMM), June 2008. Tucson, AZ.
- Static Error
Detection Using Semantic Inconsistency Inference
Isil Dillig,
Thomas Dillig, Alex Aiken. Proceedings of the Conference on Programming Language
Design and Implementation (PLDI), pages 435-446, June 2007. San Diego, CA.
- An Overview of the Saturn
Project
A. Aiken, S. Bugrara, I. Dillig, T. Dillig, P. Hawkins and
B. Hackett. Proceedings of the Workshop on Program Analysis for Software Tools
and Engineering (PASTE), pages 43-48, June 2007. San Diego, CA.
- The Saturn Program Analysis
System.
A. Aiken, S. Bugrara, I. Dillig, T. Dillig, B. Hackett, and
P. Hawkins. Stanford University Computer Science Technical Report, December
2006.
- Publishing Content on the Web:
Content Management Fitting Any Structure
Isil Dillig, Thomas
Dillig. Stanford Undergraduate Research Journal, Spring 2005.
- Inductive Invariant Generation via Abductive Inference
Conference talk, OOPSLA 2013.
- Synthesis of Circular Compositional Program Proofs via Abduction
Conference talk, TACAS 2013.
- Precise Reasoning for Programs Using Containers
Conference talk, POPL 2011.
- Symbolic Heap Abstraction with Demand-Driven Axiomatization of Memory Invariants
Conference talk, OOPSLA 2010.
- Small Formulas for Large Programs: On-line Constraint Simplification in Scalable Static Analysis
Conference talk, SAS 2010.
- Fluid Updates: Beyond Strong vs. Weak Updates
Conference talk, ESOP 2010.
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
Conference talk, CAV 2009.
- Constraint-Based Analysis in the Presence of Uncertainty and Imprecision
Invited talk at Microsoft Research, Redmond, February 2009.
- Sound, Complete, and Scalable Path-Sensitive Analysis
Conference talk, PLDI 2008.
- The CLOSER: Automating Resource Management in Java
Conference talk, ISMM 2008.
- Static Error Detection Using Semantic Inconsistency Inference
Conference talk, PLDI 2007.
Me and Isil are the developers of the following projects:
- Compass: Precise, scalable, and modular analysis of unbounded data structures such as arrays and containers.
Download Compass
- Mistral: SMT Solver providing on-line simplification of constraints.
- SAIL: Static analysis frontend based on GCC 4.3. Available under the BSD license at the project website.
I was also a member of the following projects: