|
Işıl DilligPronunciation Guide
Assistant Professor
|
| Contact |
E-mail: idillig@cs.wm.edu
Address:
College of William & Mary
Computer Science Department
McGlothlin-Street Hall 111
Williamsburg, VA 23185
| Biographical Sketch |
I am an assistant professor at the Computer Science department of the College of William & Mary . My main research interests are program analysis and verification, formal methods, and automated logical reasoning. The overarching goal of my research is to make software systems more reliable, secure, and easier to build in a robust way.
I obtained my PhD in computer science from Stanford University in 2011, where I was advised by Alex Aiken . I also received my bachelor's degree in computer science from Stanford University in 2006. My CV is available here .
| What's New |
I am looking for motivated PhD students to work with!
If you share my research interests, enjoy doing theoretical work with practical and useful applications, and like building software systems, then please do not hesitate to contact me!
| Research |
My main research interests are static program analysis/verification and automated logical reasoning.
I am interested in developing tools and novel techniques to make software systems more secure and reliable.
In particular, my research focuses on automatically proving the absence of certain classes of errors (such as memory safety errors, assertion failures, etc.) in software.
More specifically, my research tackles the challenge of
designing program analysis algorithms that are both sound (i.e., never miss any potential program errors) as well as precise (i.e., do not report a lot of false alarms) and scalable (i.e., work on large programs). My recent research has addressed scalable techniques for static reasoning about
pointers, path- and context-sensitive analysis, container data structures, the interplay between over- and under-approximations of program behavior, and constraint solving and simplification techniques that enable more efficient analysis algorithms.
| Teaching |
- 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. [slides]
- Automated Error Diagnosis Using Abductive Inference. Isil Dillig, Thomas Dillig, Alex Aiken. Programming Languages Design and Implementation (PLDI) 2012. [Extended version] [slides] [poster]
- Precise and Automatic Verification of Container Manipulating Programs PhD Thesis, Stanford University Computer Science Department, 2011.
- 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. [Full version] [slides] - Cuts from Proofs: A
Complete and Practical Technique for Solving Linear Inequalities over Integers
Isil Dillig, Thomas Dillig, Alex Aiken. Formal Methods in System Design (FMSD) CAV 2009 special issue. - Precise and Compact Modular Procedure Summaries for Heap
Manipulating Programs
Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv. Proceedings of the Conference on Programming Language Design and Implementation (PLDI) 2011. [slides] - Precise Reasoning for Programs Using Containers
Isil Dillig, Thomas Dillig, Alex Aiken. Principles of Programming Languages (POPL) 2011. [slides] - Symbolic Heap Abstraction with Demand-Driven Axiomatization of Memory Invariants
Isil Dillig, Thomas Dillig, Alex Aiken. Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2010. [slides] - 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. [slides] - 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)
Slides: [odp version] [pdf version] - 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. [slides] - 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. [slides] - 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. [slides] - 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. [slides] - 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. - "A Flow-, Path-, and Context-Sensitive Null Dereference Analysis for C Programs". Isil Dillig. Undergraduate Honors Thesis, Stanford University, June 2006.
- Publishing Content on the Web:
Content Management Fitting Any Structure
Isil Dillig, Thomas Dillig. Stanford Undergraduate Research Journal, Spring 2005.
| Students |
- Boyang Li (PhD student)
| Service |
- ESOP 2014 Program Committee
- Chair of PLDI 2013 Student Research Competition
- SAS 2013 Program Committee
- Chair of OOPSLA 2013 Student Research Competition
- OOPSLA 2013 Extended Review Committee
- POPL 2013 Program Committee
- OOPSLA 2012 Program Committee
- PLDI SRC 2012 Judging Committee
| Talks |
- "Minimum Satisfying Assignments for SMT". CAV 2012, Berkeley, CA.
- "Automated Error Diagnosis Using Abductive Inference". PLDI 2012, Beijing, China.
- "Precise Reasoning for Programs Using Containers". POPL 2011, Austin, TX, USA.
- "Symbolic Heap Abstraction with Demand-Driven Axiomatization of Memory Invariants". OOPSLA 2010, Reno, NV, USA.
- "Small Formulas for Large Programs: Constraint Simplification for Scalable Static Analysis". Static Analysis Symposium (SAS) 2010, Perpignan, France.
- "Fluid Updates: Beyond Strong vs. Weak Updates". European Symposium on Programming (ESOP) 2010, Paphos, Cyprus.
- "Cuts from Proofs: A
Complete and Practical Technique for Solving Linear Inequalities over
Integers". International Conference on Computer-Aided Verification (CAV) 2009, Grenoble, France.
- "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". Programming Language Design and Implementation (PLDI) 2008, Tucson, AZ.
- "The CLOSER: Automating
Resource Management in Java". International Symposium on Memory Management (ISMM) 2008, Tucson, AZ.
- "Static Error Detection
Using Semantic Inconsistency Inference". Programming Language Design and Implementation (PLDI) 2007, San Diego, CA.
| Software Projects |
- COMPASS Program Verification System. On-going work, co-developed with Thomas Dillig.
- Mistral SMT solver available under GPL license from here .
- SAIL program analysis front-end for C and C++. Co-developed with Thomas Dillig and Roy Frostig. Available under BSD license from here .
- SATURN program analysis system. Contributing PhD students: Brian Hackett, Yichen Xie, Peter Hawkins, Suhabe Bugrara, Thomas Dillig, and Isil Dillig. Available under BSD license from here.
| Awards |
- Distinguished Reviewer Award, OOPSLA 2012
- Stanford Graduate Fellowship, 2008-2010.
- Forbes School of Engineering Fellowship, 2006-2007.
- Wegbreit Award for the best undergraduate honors thesis in computer science. Stanford University, 2006.
- Firestone Medal for excellence in undergraduate research. Stanford University, 2006.
- Frederick Emmons Terman Engineering Scholatic Award for outstanding achievement in engineering. Stanford University, 2006.
- Mary Mills Patrick Award for highest GPA at Robert College, Istanbul, 2002.
- Dora Aksoy Award for Excellence in Mathematics. Robert College, Istanbul, 2002.
I am originally from Istanbul, Turkey. I am married to Thomas Dillig , who is also an assistant professor in computer science at William & Mary.
I'm an avid nature and outdoor photographer, and some of my photographs are available here . I also really enjoy hiking and being outdoors.
My Photography
Tom's webpage
College of William & Mary
William & Mary Computer Science Department
Stanford University
Stanford
University Computer Science Department
New York Times
Slashdot
Robert College (my high school)
PhD Comics
My first name is pronounced as "Ishil" rather than "Isil".