Thomas Dillig

• Contact
|
• News
|
• About Me
|
• Students
|
• Research
|
• Publications
|
• Talks
|
• Projects
|
• Personal

Thomas Dillig Assistant Professor Computer Science College of William & Mary

I am an Assistant Professor at the College of William & Mary.
I graduated with a PhD in Computer Science from Stanford University in 2011.


This semester I am teaching CS312 - Programming Languages

This fall I taught CS780 - Program Verification


My CV

• Haiyan Zhu, PhD Student

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.

• 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.

• 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.
• 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:

• Saturn: Precise and scalable software analysis, project website .

I am married to Isil Dillig, also a Professor in Computer Science at William & Mary. In our spare time, we both like to take pictures.