publications

2025

1. Inductive First-Order Formula Synthesis by ASP: a Case Study in Invariant Inference

   Ziyi Yang, George Pîrlea, and Ilya Sergey

   ICLP 2025. EPTCS.

   PDF Artifact
2. Veil: A Framework for Automated and Interactive Verification of Transition Systems

   George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey

   CAV 2025. Springer.

   PDF Code Artifact
3. Accelerating Automated Program Verifiers by Automatic Proof Localization

   Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Müller, Markus Püschel, and Ilya Sergey

   CAV 2025. Springer.

   PDF Artifact
4. Inductive Synthesis of Inductive Heap Predicates

   Ziyi Yang, and Ilya Sergey

   Proc. ACM Program. Lang. 2025. (OOPSLA), ACM.

   PDF arXiv Artifact
5. Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis

   Yuxi Ling, Gokul Rajiv, Kiran Gopinathan, and Ilya Sergey

   USENIX Security Symposium 2025. USENIX Association.

   PDF Artifact

2024

1. Concurrent Data Structures Made Easy

   Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, and Ilya Sergey

   Proc. ACM Program. Lang. 2024. (OOPSLA), ACM.

   PDF arXiv Code Artifact Slides
2. DSLs in Racket: You Want It How, Now?

   Yunjeong Lee, Kiran Gopinathan, Ziyi Yang, Matthew Flatt, and Ilya Sergey

   SLE 2024. ACM.

   PDF Artifact
3. Compositional Verification of Composite Byzantine Protocols

   Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey

   31st ACM Conference on Computer and Communications Security (CCS’24) 2024. ACM.

   PDF Code Artifact
4. Higher-Order Specifications for Deductive Synthesis of Programs with Pointers

   David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin

   ECOOP 2024. LIPIcs, Schloss Dagstuhl.

   PDF arXiv Code Artifact
5. Mechanised Hypersafety Proofs about Structured Data

   Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

   Proc. ACM Program. Lang. 2024. (PLDI), ACM.

   PDF arXiv Code Artifact
6. Small Scale Reflection for the Working Lean User

   Vladimir Gladshtein, George Pîrlea, and Ilya Sergey

   2024. Unpublished draft.

   arXiv Code Artifact
7. Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic

   Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey

   CPP 2024. ACM.

   Distinguished Paper Award

   PDF Code Artifact Slides

2023

1. Greybox Fuzzing of Distributed Systems

   Ruijie Meng, George Pîrlea, Abhik Roychoudhury, and Ilya Sergey

   30th ACM Conference on Computer and Communications Security (CCS’23) 2023. ACM.

   PDF Code
2. Adventure of a Lifetime: Extract Method Refactoring for Rust

   Sewen Thy, Andreea Costea, Kiran Gopinathan, and Ilya Sergey

   Proc. ACM Program. Lang. 2023. (OOPSLA), ACM.

   PDF Artifact
3. Mostly Automated Proof Repair for Verified Libraries

   Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

   Proc. ACM Program. Lang. 2023. (PLDI), ACM.

   ACM SIGPLAN Distinguished Paper Award

   PDF Code Artifact Slides Video Website
4. Leveraging Rust Types for Program Synthesis

   Jonáš Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, and Ilya Sergey

   Proc. ACM Program. Lang. 2023. (PLDI), ACM.

   Distinguished Artifact Award

   PDF Extended Version Artifact Slides Video
5. Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112)

   Swen Jacobs, Kenneth L. McMillan, Roopsha Samanta, and Ilya Sergey

   Dagstuhl Reports 2023. Vol. 13, (3), Pages 32–48.

   PDF
6. Hippodrome: Data Race Repair using Static Analysis Summaries

   Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, and Ilya Sergey

   ACM Trans. Softw. Eng. Methodol. 2023. Vol. 32, (2), ACM.

   PDF Code Artifact

2022

1. Random Testing of a Higher-Order Blockchain Language (Experience Report)

   Tram Hoang, Anton Trunov, Leonidas Lampropoulos, and Ilya Sergey

   Proc. ACM Program. Lang. 2022. (ICFP), ACM.

   PDF Artifact Slides
2. Towards Optimising Certified Programs by Proof Rewriting

   Kiran Gopinathan, and Ilya Sergey

   EGRAPHS 2022. Informal Proceedings.

   PDF Slides

2021

1. Certifying the Synthesis of Heap-Manipulating Programs

   Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, and Ilya Sergey

   Proc. ACM Program. Lang. 2021. (ICFP), ACM.

   PDF Artifact Slides Video
2. The Next 700 Smart Contract Languages

   Ilya Sergey

   Principles of Blockchain Systems 2021. Morgan & Claypool. Author’s version.

   PDF
3. Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities (Invited Paper)

   Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben Rowe, and Ilya Sergey

   CAV 2021. LNCS, Vol. 12759, Springer.

   PDF Artifact
4. Cyclic Program Synthesis

   Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben Rowe, and Ilya Sergey

   PLDI 2021. ACM.

   ACM SIGPLAN Distinguished Paper Award

   PDF Extended Version Artifact
5. Practical Smart Contract Sharding with Ownership and Commutativity Analysis

   George Pîrlea, Amrit Kumar, and Ilya Sergey

   PLDI 2021. ACM.

   PDF Artifact
6. Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis

   Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, and Wei-Ngan Chin

   VMCAI 2021. LNCS, Vol. 12597, Springer.

   PDF Artifact
7. Protocol Combinators for Modeling, Testing, and Execution of Distributed Systems

   Kristoffer Just Arndal Andersen, and Ilya Sergey

   J. Funct. Program. 2021. Vol. 31, Cambridge University Press.

   PDF Code

2020

1. Certifying Certainty and Uncertainty in Approximate Membership Query Structures

   Kiran Gopinathan, and Ilya Sergey

   CAV 2020. LNCS, Vol. 12225, Springer.

   PDF Code Artifact Blog Slides Video
2. Compiling a Higher-Order Smart Contract Language to LLVM

   Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pîrlea, Amrit Kumar, and Ilya Sergey

   CoRR 2020. Accepted to 2020 Virtual LLVM Developers Meeting.

   PDF arXiv Poster
3. Concise Read-Only Specifications for Better Synthesis of Programs with Pointers

   Andreea Costea, Amy Zhu, Nadia Polikarpova, and Ilya Sergey

   ESOP 2020. LNCS, Vol. 12075, Springer.

   PDF Code Artifact

2019

1. QED at Large: A Survey of Engineering of Formally Verified Software

   Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock

   Found. Trends Program. Lang. 2019. Vol. 5, (2-3), now Publishers.

   PDF Errata
2. Safer Smart Contract Programming with Scilla

   Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao

   Proc. ACM Program. Lang. 2019. (OOPSLA), ACM.

   Distinguished Artifact Award

   PDF Code Artifact Slides Video
3. Exploiting the laws of order in smart contracts

   Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, and Prateek Saxena

   ISSTA 2019. ACM.

   PDF Artifact
4. Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis

   Elvira Albert, Pablo Gordillo, Albert Rubio, and Ilya Sergey

   VECoS 2019. LNCS, Vol. 11847, Springer.

   PDF Artifact
5. Engineering Distributed Systems that We Can Trust (and Also Run)

   Ilya Sergey

   PODC 2019. ACM. Invited Talk.

   PDF
6. Distributed Protocol Combinators

   Kristoffer Just Arndal Andersen, and Ilya Sergey

   PADL 2019. LNCS, Vol. 11372, Springer.

   PDF Code
7. Structuring the Synthesis of Heap-Manipulating Programs

   Nadia Polikarpova, and Ilya Sergey

   Proc. ACM Program. Lang. 2019. (POPL), ACM.

   ACM SIGPLAN Distinguished Paper Award

   PDF arXiv Code Artifact Slides Video
8. A True Positives Theorem for a Static Race Detector

   Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey

   Proc. ACM Program. Lang. 2019. (POPL), ACM.

   PDF arXiv Artifact Slides
9. Towards Mechanising Probabilistic Properties of a Blockchain

   Kiran Gopinathan, and Ilya Sergey

   CoqPL 2019. Informal Proceedings.

   PDF Code Slides

2018

1. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale

   Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor

   ACSAC 2018. ACM.

   PDF Code
2. RacerD: compositional static race detection

   Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey

   Proc. ACM Program. Lang. 2018. (OOPSLA), ACM.

   PDF Video
3. Paxos Consensus, Deconstructed and Abstracted

   ‪Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, and Ilya Sergey

   ESOP 2018. LNCS, Vol. 10801, Springer.

   PDF Extended Version Code
4. Temporal Properties of Smart Contracts

   Ilya Sergey, Amrit Kumar, and Aquinas Hobor

   ISoLA 2018. LNCS, Vol. 11247, Springer.

   PDF
5. Mechanising Blockchain Consensus

   George Pîrlea, and Ilya Sergey

   CPP 2018. ACM.

   PDF Code Slides
6. Programming and Proving with Distributed Protocols

   Ilya Sergey, James R. Wilcox, and Zachary Tatlock

   Proc. ACM Program. Lang. 2018. (POPL), ACM.

   PDF Code Slides
7. Scilla: a Smart Contract Intermediate-Level LAnguage

   Ilya Sergey, Amrit Kumar, and Aquinas Hobor

   CoRR 2018. Vol. abs/1801.00687, Technical Report.

   arXiv
8. Automatic Inference of Gas Bounds for Smart Contracts on the Ethereum Blockchain

   Elvira Albert, Albert Rubio, Ilya Sergey, and Thomas Sibut-Pinote

   2018. Unpublished draft.

   PDF

2017

1. Modular, higher order cardinality analysis in theory and practice

   Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones, and Joachim Breitner

   J. Funct. Program. 2017. Vol. 27, Cambridge University Press.

   PDF
2. Concurrent Data Structures Linked in Time

   Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee

   ECOOP 2017. LIPIcs, Vol. 74, Schloss Dagstuhl.

   PDF arXiv Artifact
3. A Concurrent Perspective on Smart Contracts

   Ilya Sergey, and Aquinas Hobor

   1st Workshop on Trusted Smart Contracts 2017. LNCS, Vol. 10323, Springer.

   PDF Slides
4. Programming Language Abstractions for Modularly Verified Distributed Systems

   James R. Wilcox, Ilya Sergey, and Zachary Tatlock

   SNAPL 2017. LIPIcs, Vol. 71, Schloss Dagstuhl.

   PDF Slides

2016

1. Hoare-Style Specifications as Correctness Conditions for Non-Linearizable Concurrent Objects

   Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco

   OOPSLA 2016. ACM.

   PDF arXiv Slides Video
2. Operational Aspects of C/C++ Concurrency

   Anton Podkopaev, Ilya Sergey, and Aleksandar Nanevski

   CoRR 2016. Vol. abs/1606.01400, Working Draft.

   arXiv
3. Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms

   Ilya Sergey

   ICFP 2016. ACM.

   PDF Slides Video

2015

1. Mechanized Verification of Fine-Grained Concurrent Programs

   Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee

   PLDI 2015. ACM.

   PDF Slides Video Website
2. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity

   Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee

   ESOP 2015. LNCS, Vol. 9032, Springer.

   PDF arXiv Extended Version Slides

2014

1. Pushdown flow analysis with abstract garbage collection

   J. Ian Johnson, Ilya Sergey, Christopher Earl, Matthew Might, and David Van Horn

   J. Funct. Program. 2014. Vol. 24, (2-3), Cambridge University Press.

   PDF
2. Communicating State Transition Systems for Fine-Grained Concurrent Resources

   Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco

   ESOP 2014. LNCS, Vol. 8410, Springer.

   PDF Extended Version Slides Website
3. Modular, Higher-Order Cardinality Analysis in Theory and Practice

   Ilya Sergey, Dimitrios Vytiniotis, and Simon L. Peyton Jones

   POPL 2014. ACM.

   PDF Extended Version Slides
4. Deriving Interpretations of the Gradually-Typed Lambda Calculus

   Álvaro García-Pérez, Pablo Nogueira, and Ilya Sergey

   PEPM 2014. ACM.

   PDF
5. Introducing Functional Programmers to Interactive Theorem Proving and Program Verification

   Ilya Sergey, and Aleksandar Nanevski

   2014. Unpublished draft.

   PDF

2013

1. Monadic abstract interpreters

   Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens

   PLDI 2013. ACM.

   PDF Code Slides
2. Fixing Idioms: a Recursion Primitive for Applicative DSLs

   Dominique Devriese, Ilya Sergey, Dave Clarke, and Frank Piessens

   PEPM 2013. ACM.

   PDF Slides
3. Ownership Types: A Survey

   Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad

   Aliasing in Object-Oriented Programming. Types, Analysis and Verification 2013. LNCS, Vol. 7850, Springer.

   PDF

2012

1. Operational Aspects of Type Systems

   Ilya Sergey

   PhD Thesis. KU Leuven, Leuven, Belgium. 2012.

   PDF Slides Website
2. A correspondence between type checking via reduction and type checking via evaluation

   Ilya Sergey, and Dave Clarke

   Inf. Process. Lett. 2012. Vol. 112, (1-2),

   PDF Code
3. Gradual Ownership Types

   Ilya Sergey, and Dave Clarke

   ESOP 2012. LNCS, Vol. 7211, Springer.

   PDF Code Slides
4. Introspective Pushdown Analysis of Higher-Order Programs

   Christopher Earl, Ilya Sergey, Matthew Might, and David Van Horn

   ICFP 2012. ACM.

   PDF Slides Video
5. Calculating Graph Algorithms for Dominance and Shortest Path

   Ilya Sergey, Jan Midtgaard, and Dave Clarke

   MPC 2012. LNCS, Vol. 7342, Springer.

   PDF Slides
6. Theory and Practice of Demand Analysis in Haskell

   Ilya Sergey, Simon L. Peyton Jones, and Dimitrios Vytiniotis

   2012. Unpublished draft.

   PDF

2011

1. From type checking by recursive descent to type checking with an abstract machine

   Ilya Sergey, and Dave Clarke

   LDTA 2011. ACM.

   PDF Code Slides
2. Implementation of Gradual Ownership Types for Java using Attribute Grammars

   Ilya Sergey

   Software Engineering. 2011. Vol. 6, Saint Petersburg State University Publishing. In Russian.

   PDF

2010

1. Automatic refactorings for Scala programs

   Ilya Sergey, Dave Clarke, and Alexander Podkhalyuzin

   The First Scala Workshop – Scala Days 2010. Informal Proceedings.

   PDF Video
2. Scripting an IDE for EDSL Awareness

   Ilya Sergey, Peter Gromov, and Dave Clarke

   2010. Unpublished draft.

   PDF

2009

1. A Semantics for Context-Oriented Programming with Layers

   Dave Clarke, and Ilya Sergey

   First International Workshop on Context-Oriented Programming (COP) 2009. ACM.

   PDF Slides

2008

1. Implementation of JVM-based languages support in IntelliJ IDEA

   Ilya Sergey

   International Workshop Workshop on Multiparadigm Programming with Object-Oriented Languages (MPOOL) 2008. Informal Proceedings.

   PDF
2. Extraction of Musical Notation from a Musical Signal

   Ilya Sergey

   MSc Thesis. Saint Petersburg State University, Russia. 2008. In Russian.

   PDF Slides