Publications

Recent Publications

 

• Relational Verification using Reinforcement Learning. Jia Chen, Jiayi Wei, Yu Feng, Osbert Bastani, Isil Dillig. To appear in OOPSLA’19.

 

• Optimization + Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness.Greg Anderson, Shankara Pailoor, Isil Dillig, Swarat Chaudhuri. In PLDI’19. (Distinguished paper award)

 

• Synthesizing Database Applications for Schema Refactoring Yuepeng Wang, James Dong, Rushi Shah, Isil Dillig. In PLDI’19.

 

• Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. In VSTTE’19.

 

• Trinity: An Extensible Synthesis Framework for Data Science. Jia Chen, Ruben Martins, Yanju Chen, Yu Feng, Isil Dillig. In VLDB’19.

 

• Relational Program Synthesis. Yuepeng Wang, Xinyu Wang, Isil Dillig. In OOPSLA’18.

 

• Verified Three-Way Program Merge. Marcelo Sousa, Isil Dillig, Shuvendu Lahiri. In OOPSLA’18.

 

• Singularity: Pattern Fuzzing for Worst Case Complexity. Jiayi Wei, Jia Chen, Yu Feng, Kostas Ferles, Isil Dillig. To appear in FSE’18.

 

• Learning Abstractions for Program Synthesis. Xinyu Wang, Greg Anderson, Isil Dillig, Ken McMillan. In CAV’18.

 

• Symbolic Reasoning for Automatic Signal Placement. Kostas Ferles, Jacob Van Geffen, Isil Dillig, Yannis Smaragdakis. In PLDI’18. [Extended version]

 

• Program Synthesis using Conflict-Driven Learning. Yu Feng, Ruben Martins, Osbert Bastani, Isil Dillig. In PLDI’18. (Distinguished paper award)

 

• Automated Migration of Hierarchical Data to Relational Tables using Programming-by-Example. Navid Yaghmazadeh, Xinyu Wang, Isil Dillig. To appear in VLDB’18.

 

• Program Synthesis using Abstraction Refinement. Xinyu Wang, Isil Dillig, Rishabh Singh. In POPL’18.

 

• Verifying Equivalence of Database-Driven Applications. Yuepeng Wang, Isil Dillig, Shuvendu Lahiri, William Cook. In POPL’18.

 

• Precise Detection of Side-Channel Vulnerabilities using Quantitative Cartesian Hoare Logic. Jia Chen, Yu Feng, Isil Dillig. In CCS’17.

 

• Synthesis of Data Completion Scripts using Finite Tree Automata . Xinyu Wang, Isil Dillig, Rishabh Singh. In OOPSLA’17.

 

• SQLizer: Query Synthesis from Natural Language . Navid Yaghmazadeh, Yuepeng Wang, Isil Dillig, Thomas Dillig. In OOPSLA’17.

 

•  Failure-Directed Program Trimming. Kostas Ferles, Valentin Wuestholz, Maria Christakis, Isil Dillig. In FSE 2017.

 

• Component-based Synthesis of Table Consolidation and Transformation Tasks from Examples. Yu Feng, Ruben Martins, Jacob VanGeffen, Isil Dillig, Swarat Chaudhuri. In PLDI’17. [Watch Matrix-themed video!]

 

• Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions. Valentin Wuestholz, Oswaldo Olivo, Marijn Heule, Isil Dillig. In TACAS’17. Best paper award

 

• Automated Synthesis of Semantic Malware Signatures using Maximum Satisfiability. Yu Feng, Osbert Bastani, Ruben Martins, Isil Dillig, Saswat Anand. In NDSS’17.

 

•  Component-Based Synthesis for Complex APIs. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Tom Reps. In POPL’17.

 

• Hunter: Type-Directed Code Reuse Using Integer Linear Programming. Yuepeng Wang, Yu Feng, Ruben Martin, Arati Kaushik, Isil Dillig, Steven Reiss. In FSE’16.

 

• Cartesian Hoare Logic for Verifying k-safety Properties. Marcelo Sousa, Isil Dillig. In PLDI’16.

 

• Synthesizing Transformations on Hierarchically Structured Data. Navid Yaghmazadeh, Chris Klinger, Isil Dillig, Swarat Chaudhuri. In PLDI’16.

 

• Maximal Specification Synthesis. Aws Albarghouthi, Isil Dillig, Arie Gurfinkel. In POPL’16.

 

• Bottom-up Context-Sensitive Pointer Analysis for Java. Yu Feng, Xinyu Wang, Isil Dillig, Thomas Dillig. In APLAS 2015.

 

• Detecting and Exploiting Second Order Denial of Service Vulnerabilities in Web Applications Oswaldo Olivo, Isil Dillig, Calvin Lin. In CCS 2015.

 

• EXPLORER : Query- and Demand-Driven Exploration of Interprocedural Control Flow Properties. Yu Feng, Xinyu Wang, Isil Dillig, Calvin Lin. In OOPSLA 2015.

 

• Synthesizing Data Structure Transformations from Input-Output Examples. John Feser, Swarat Chaudhuri, Isil Dillig. PLDI 2015.

 

• Static Detection of Asymptotic Performance Bugs in Collection Traversals. Oswaldo Olivo, Isil Dillig, Calvin Lin. PLDI 2015.

 

• Apposcopy: Semantics-Based Detection of Android Malware Through Static Analysis. Yu Feng, Saswat Anand, Isil Dillig, Alex Aiken. FSE 2014.

 

• Optimal Guard Synthesis for Memory Safety. Thomas Dillig, Isil Dillig, Swarat Chaudhuri. CAV 2014.

 

• 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. In TACAS 2013.