Işıl Dillig

Işıl Dillig's Publications

2025

  • Automated Verification of Consistency in Zero-Knowledge Proof Circuits. Jon Stephens, Shankara Pailoor, Isil Dillig. In CAV 2025.
  • Integer Reasoning Modulo Different Constants in SMT. Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Işil Dillig, Clark Barrett. In CAV 2025.
  • Graphiti: Bridging Graph and Relational Database Queries. Yang He, Ruijie Fang, Isil Dillig, Yuepenag Wang. In PLDI 2025.
  • SYNAPSE: SYmbolic Neural-Aided Preference Synthesis Engine. Sadanand Modak, Noah Patton, Isil Dillig, Joydeep Biswas. In AAAI 2025.
  • Copper and Wire: Bridging Expressiveness and Performance for Service Mesh Policies. Divyanshu Saxena, William Zhang, Shankara Pailoor, Isil Dillig, Aditya Akella. In ASPLOS 2025.

    • 2024

  • Dynamic Model Predictive Shielding for Provably Safe Reinforcement Learning. Arko Banarjee, Kia Rahmani, Joydeep Biswas, Isil Dillig. In Neurips 2024.
  • Control-Flow Deobfuscation using Trace-Informed Compositional Program Synthesis. Ben Mariano, Zetten Wang, Shankara Pailoor, Christian Collberg, Isil Dillig. In OOPSLA 2024.
  • Split Gröbner Bases for Satisfiability Modulo Finite Fields. Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett and Isil Dillig. In CAV 2024.
  • Relational Synthesis of Recursive Programs via Constrained Tree Automata. Anders Miltner, Zetten Wang, Swarat Chaudhuri, Isil Dillig. In CAV 2024.
  • From Batch to Stream: Automatic Generation of Online Algorithms. Zetten Wang, Shankara Pailoor, Aaryan Prakash, Yuepeng Wang, Isil Dillig. In PLDI 2024.
  • Programmatic Imitiation Learning from Unlabeled and Noisy Demonstrations. Jimmy Xin, Linus Zheng, Kia Rahmani, Jiayi Wei, Jarrett Holtz, Isil Dillig, Joydeep Biswas. In IEEE Robotics and Automation Letters (RA-L) 2024.
  • PhotoScout: Synthesis-Powered Multi-Modal Image Search. Celeste Barnaby, Jocelyn Chen, Chenglong Wang, Isil Dillig. In CHI 2024.
  • Coeditor: Leveraging Repo-level Diffs for Code Auto-editing. Jiayi Wei, Greg Durrett, Isil Dillig. In ICLR 2024. (Spotlight)
  • Semantic Code Refactoring for Abstract Data Types. Shankara Pailoor, Yuepeng Wang, Isil Dillig. In POPL 2024.
  • Programming-by-Demonstration for Long-Horizon Robot Tasks. Noah Patton, Kia Rahmani, Meghana Missula, Joydeep Biswas, Isil Dillig. In POPL 2024.
  • Certifying Zero-Knowledge Proofs with Refinement Types. Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, Isil Dillig, Yu Feng. In IEEE Security & Privacy 2024 (Oakland)

    • 2023

  • Satisfiability-Aided Language Models using Declarative Prompting . Xi Ye, Jocelyn Chen, Isil Dillig, Greg Durrett. In Neurips 2023.
  • Data Extraction via Semantic Regular Expression Synthesis. Jocelyn Chen, Arko Banarjee, Cagatay Demiralp, Greg Durrett, Isil Dillig. In OOPSLA'23.
  • Inductive Program Synthesis Guided by Observational Program Similarity. Jack Feser, Isil Dillig, Armando Solar-Lezama. In OOPSLA'23.
  • Practical Security Analysis of Zero Knowledge Proof Circuits. Hongbo Wen, Jon Stephens, Yanju Chen, Kostas Ferles, Shankara Pailoor, Kyle Charbonnet, Isil Dillig, Yu Feng. In Usenix Security 2023
  • ImageEye: Batch Image Processing Using Program Synthesis. Celeste Barnaby, Jocelyn Chen, Roopsha Samanta, Isil Dillig. In PLDI'23
  • Automated Detection of Under-constrained Circuits in Zero-Knowledge Proofs. Shankara Pailoor, Yanju Chen, Franklin Wang, Clara Rodríguez, Jacob Van Geffen, Jason Morton, Michael Chu, Brian Gu, Yu Feng, Isil Dillig. In PLDI'23
  • Guiding Safe Exploration with Weakest Preconditions. Greg Anderson, Swarat Chaudhuri, Isil Dillig. In ICLR'23.
  • TypeT5: Seq2seq Type Inference using Static Analysis. Jiayi Wei, Greg Durrett, Isil Dillig. In ICLR'23.
  • Automated Translation of Functional Big Data Queries to SQL. Guoqiang Zhang, Ben Mariano, Xipeng Shen, Isil Dillig. In OOPSLA'23.
  • Chipmunk: Investigating Crash-Consistency in Persistent-Memory File Systems. Hayley LeBlanc, Shankara Pailoor, Om Saran K R E, Isil Dillig, James Bornholt, Vijay Chidambaram. In EuroSys 2023. (Best paper award)

    • 2022

  • Learning Contract Invariants using Reinforcement Learning. Junrui Liu, Yanju Chen, Bryan Tan, Isil Dillig, Yu Feng. In ASE'22.
  • Type-Directed Synthesis of Visualizations from Natural Language Queries. Jocelyn Chen, Shankara Pailoor, Celeste Barnaby, Abby Criswell, Chenglong Wang, Greg Durrett, Isil Dillig. In OOPSLA'22.
  • Synthesis Powered Optimization of Smart Contracts vis Data Type Refactoring. Yuepeng Wang, Yanju Chen, Maruth Goyal, James Dong, Yu Feng, Isil Dillig. In OOPSLA'22
  • STEADY: Simultaneous State Estimation and Dynamics Learning from Indirect Observations. Jiayi Wei, Jarrett Holz, Isil Dillig, Joydeep Biswas. In IROS'22.
  • Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis. Ben Mariano, Yanju Chen, Yu Feng, Greg Durrett, Isil Dillig. In OOPSLA'22. [Extended version]
  • Synthesizing Fine-Grained Synchronization Protocols for Implicit Signal Monitors. Kostas Ferles, Ben Sepanski, Rahul Krishnan, James Bornholt, Isil Dillig. In OOPSLA'22. [Extended version]
  • Counterfactal Explanations for Models of Code. Juergen Cito, Isil Dillig, Vijay Murali, Satish Chandra. In ICSE'22 (industry track)
  • Bottom-up Synthesis of Recursive Functional Programs using Angelic Execution. Anders Miltner, Adrian Trejo Nunez, Ana Brendel, Swarat Chaudhuri, Isil Dillig. In POPL'22. (Distinguished Paper Award)
  • SolType: Refinement Types for Solidity. Bryan Tan, Ben Mariano, Shuvendu Lahiri, Isil Dillig, Yu Feng. In POPL'22.

    • 2021

  • Optimal Neural Program Synthesis from Multimodal Specifications. Xi Ye, Jocelyn Chen, Isil Dillig, Greg Durrett. In EMNLP Findings 2021.
  • UDF to SQL Translation Through Compositional Lazy Inductive Synthesis. Guoqiang Zhang, Yuanchao Xu, Xipeng Shen, Isil Dillig. In OOPSLA 2021.
  • OneVision: Centralized to Distributed Controller Synthesis with Delay Compensation. Jiayi Wei, Tongrui Li, Swarat Chaudhuri, Isil Dillig, Joydeep Biswas. In IROS 2021.
  • Checking Conformance of Applications against GUI Policies. Zhen Zheng, Yu Feng, Mike Ernst, Sebastian Porst, Isil Dillig. In FSE 2021.
  • Explaining Mispredictions of ML Models. Jurgen Cito, Isil Dillig, Vijay Murali, Sonia Kim, Satish Chandra. In FSE 2021.
  • Synthesizing Data Structure Refinements from Integrity Constraints. Shankara Pailoor, Yuepeng Wang, Xinyu Wang, Isil Dillig. In PLDI 2021.
  • Web Question Answering with Neurosymbolic Program Synthesis. Jocelyn Chen, Aaron Lamoreaux, Xinyu Wang, Greg Durrett, Osbert Bastani, Isil Dillig. In PLDI 2021.
  • SmartPulse: Automated Checking of Temporal Properties in Smart Contracts. Jon Stephens, Kostas Ferles, Ben Mariano, Shuvendu Lahiri, Isil Dillig. In IEEE S&P (Oakland) 2021.
  • Falx: Synthesis-powered Visualization Authoring. Chenglong Wang, Yu Feng, Rastislav Bodik, Isil Dillig, Alvin Cheung, Amy J. Ko. In CHI 2021. (Best paper award)
  • Verifying Correct Usage of Context-Free API Protocols. Kostas Ferles, Jon Stephens, Isil Dillig. In POPL'21.
  • Neurosymbolic Reinforcement Learning with Formally Verified Exploration. Greg Anderson, Abhinav Verma, Isil Dillig, Swarat Chaudhui. In Neurips'21.

    • 2020

  • Demystifying Loops in Smart Contracts. Ben Mariano, Yanju Chen, Yu Feng, Shuvendu Lahiri, Isil Dillig. In ASE'20.
  • Sketch-Driven Regular Expression Generation from Natural Language and Examples Xi Ye, Jocelyn Chen, Isil Dillig, and Greg Durrett. In TACL'20.
  • Automated policy synthesis for system call sandboxing Shankara Pailoor, Xinyu Wang, Hovav Shacham, Isil Dillig. In OOPSLA 2020. (Distinguished Paper Award)
  • Program Synthesis using Deduction-Guided Reinforcement Learning. Yanju Chen, Chenglong Wang, Osbert Bastani, Isil Dillig and Yu Feng. In CAV'20.
  • Synthesizing JIT Compilers for In-Kernel DSLs. Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang and Emina Torlak. In CAV'20.
  • StructuredRegex: A New Dataset for Regex Synthesis from Natural Language and Examples Xi Ye, Jocelyn Chen, Isil Dillig and Greg Durrett. In ACL'20.
  • Multi-Modal Synthesis of Regular Expressions. Jocelyn Chen, Xinyu Wang, Xi Ye, Greg Durrett, Isil Dillig. In PLDI'20.
  • Data Migration using Datalog Program Synthesis. Yuepeng Wang, Rushi Shah, Abby Criswell, Rong Pan, Isil Dillig. In VLDB'20.
  • LambdaNet: Probabilistic Type Inference using Graph Neural Networks. Jiayi Wei, Maruth Goyal, Greg Durrett, Isil Dillig. In ICLR'20.
  • Visualization by Example. Chenglong Wang, Yu Feng, Ras Bodik, Alvin Cheung, Isil Dillig. In POPL'20.

    • 2019

  • Relational Verification using Reinforcement Learning. Jia Chen, Jiayi Wei, Yu Feng, Osbert Bastani, Isil Dillig. 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.

    • 2018

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

    • 2017

  • Precise Detection of Side-Channel Vulnerabilities using Quantitative Cartesian Hoare Logic. Jia Chen, Yu Feng, Isil Dillig. In CCS'17.
  • Static Detection of Asymptotic Side Channel Vulnerabilities in Web Applications. Jia Chen, Oswaldo Olivo, Isil Dillig, Calvin Lin In ASE'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. (Distinguished paper award)
  • Failure-Directed Program Trimming. Kostas Ferles, Valentin Wuestholz, Maria Christakis, Isil Dillig. In FSE'17.
  • Component-based Synthesis of Table Consolidation and Transformation Tasks from Examples. Yu Feng, Ruben Martins, Jacob VanGeffen, Isil Dillig, Swarat Chaudhuri. In PLDI'17. [video]
  • Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions. Valentin Wuestholz, Oswaldo Olivo, Marijn Heule, Isil Dillig. In TACAS'17. [Extended version] (ETAPS'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. [Extended version]

    • 2016

  • Hunter: Type-Directed Code Reuse using Integer Linear Programming. Yuepeng Wang, Yu Feng, Ruben Martins, Arati Kaushik, Isil Dillig, Steven P. Reiss. In FSE'16. [Long version]
  • Cartesian Hoare Logic for Verifying k-Safety Properties. Marcelo Sousa, Isil Dillig. In PLDI'16. [Extended version]
  • Synthesizing Transformations on Hierarchically Structured Data. Navid Yaghmazadeh, Chris Klinger, Isil Dillig, Swarat Chaudhuri. In PLDI'16. [demo video]
  • Maximal Specification Synthesis. Aws Albarghouthi, Isil Dillig, Arie Gurfinkel. In POPL 2016. [Extended version]

    • 2015

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

    • 2014

  • 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. [Extended version]
  • Consolidation of Queries with User-Defined Functions . Marcelo Sousa, Isil Dillig, Dimitrios Vytionitis, Thomas Dillig, Christos Gkantsidis. PLDI 2014.

    • 2013

  • 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. Journal version in STTT'15. (Invited for journal special issue)

    • 2012

  • 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. Programming Languages Design and Implementation (PLDI) 2012. [Extended version]

    • During PhD

  • 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]
  • 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.
  • Precise Reasoning for Programs Using Containers Isil Dillig, Thomas Dillig, Alex Aiken. Principles of Programming Languages (POPL) 2011.
  • 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.
  • 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. (Invited for journal special issue)
  • SAIL: Static Analysis Intermediate Language with a Two-Level Representation Isil Dillig, Thomas Dillig, Alex Aiken. Technical Report, Stanford University 2009.
  • 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. (CACM research highlight)
  • 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.