publications

Google Scholar DBLP CSAuthors

2026

  1. Lazy Proof Automation for Separation Logic
    ITP 2026. LIPIcs, Schloss Dagstuhl.
  2. Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean
    CAV 2026. Springer.
  3. Grammar Repair with Examples and Tree Automata
    Yunjeong Lee, Gokul Rajiv, and Ilya Sergey
    Proc. ACM Program. Lang. 2026. (OOPSLA), ACM.
  4. Foundational Multi-Modal Program Verifiers
    Proc. ACM Program. Lang. 2026. (POPL), ACM.
  5. Velvet: A Multi-Modal Verifier for Effectful Programs
    Dafny Workshop 2026. Workshop paper; superseded by the CAV’26 paper.
  6. Lessons from Building an Auto-Active Verifier in Lean
    Dafny Workshop 2026. Workshop paper.

2025

  1. Beluga: Block Synchronization for BFT Consensus Protocols
    2025. Unpublished draft.
  2. Inductive First-Order Formula Synthesis by ASP: a Case Study in Invariant Inference
    Ziyi Yang, George Pîrlea, and Ilya Sergey
    ICLP 2025. EPTCS.
  3. Veil: A Framework for Automated and Interactive Verification of Transition Systems
    CAV 2025. Springer.
  4. Accelerating Automated Program Verifiers by Automatic Proof Localization
    CAV 2025. Springer.
  5. Inductive Synthesis of Inductive Heap Predicates
    Ziyi Yang, and Ilya Sergey
    Proc. ACM Program. Lang. 2025. (OOPSLA), ACM.
  6. Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis
    USENIX Security Symposium 2025. USENIX Association.

2024

  1. Concurrent Data Structures Made Easy
    Proc. ACM Program. Lang. 2024. (OOPSLA), ACM.
  2. DSLs in Racket: You Want It How, Now?
    SLE 2024. ACM.
  3. Compositional Verification of Composite Byzantine Protocols
    31st ACM Conference on Computer and Communications Security (CCS’24) 2024. ACM.
  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.
  5. Mechanised Hypersafety Proofs about Structured Data
    Proc. ACM Program. Lang. 2024. (PLDI), ACM.
  6. Small Scale Reflection for the Working Lean User
    2024. Unpublished draft.
  7. Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
    CPP 2024. ACM.
    Distinguished Paper Award

2023

  1. Greybox Fuzzing of Distributed Systems
    30th ACM Conference on Computer and Communications Security (CCS’23) 2023. ACM.
  2. Adventure of a Lifetime: Extract Method Refactoring for Rust
    Proc. ACM Program. Lang. 2023. (OOPSLA), ACM.
  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
  4. Leveraging Rust Types for Program Synthesis
    Proc. ACM Program. Lang. 2023. (PLDI), ACM.
    Distinguished Artifact Award
  5. Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112)
    Dagstuhl Reports 2023. Vol. 13, (3), Pages 32–48.
    PDF
  6. Hippodrome: Data Race Repair using Static Analysis Summaries
    ACM Trans. Softw. Eng. Methodol. 2023. Vol. 32, (2), ACM.

2022

  1. Random Testing of a Higher-Order Blockchain Language (Experience Report)
    Proc. ACM Program. Lang. 2022. (ICFP), ACM.
  2. Towards Optimising Certified Programs by Proof Rewriting
    Kiran Gopinathan, and Ilya Sergey
    EGRAPHS 2022. Informal Proceedings.

2021

  1. Certifying the Synthesis of Heap-Manipulating Programs
    Proc. ACM Program. Lang. 2021. (ICFP), ACM.
  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)
    CAV 2021. LNCS, Vol. 12759, Springer.
  4. Cyclic Program Synthesis
    PLDI 2021. ACM.
    ACM SIGPLAN Distinguished Paper Award
  5. Practical Smart Contract Sharding with Ownership and Commutativity Analysis
    George Pîrlea, Amrit Kumar, and Ilya Sergey
    PLDI 2021. ACM.
  6. Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis
    VMCAI 2021. LNCS, Vol. 12597, Springer.
  7. Protocol Combinators for Modeling, Testing, and Execution of Distributed Systems
    J. Funct. Program. 2021. Vol. 31, Cambridge University Press.

2020

  1. Certifying Certainty and Uncertainty in Approximate Membership Query Structures
    Kiran Gopinathan, and Ilya Sergey
    CAV 2020. LNCS, Vol. 12225, Springer.
  2. Compiling a Higher-Order Smart Contract Language to LLVM
    CoRR 2020. Accepted to 2020 Virtual LLVM Developers Meeting.
  3. Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
    ESOP 2020. LNCS, Vol. 12075, Springer.

2019

  1. QED at Large: A Survey of Engineering of Formally Verified Software
    Found. Trends Program. Lang. 2019. Vol. 5, (2-3), now Publishers.
  2. Safer Smart Contract Programming with Scilla
    Proc. ACM Program. Lang. 2019. (OOPSLA), ACM.
    Distinguished Artifact Award
  3. Exploiting the laws of order in smart contracts
    ISSTA 2019. ACM.
  4. Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis
    VECoS 2019. LNCS, Vol. 11847, Springer.
  5. Engineering Distributed Systems that We Can Trust (and Also Run)
    Ilya Sergey
    PODC 2019. ACM. Invited Talk.
    PDF
  6. Distributed Protocol Combinators
    PADL 2019. LNCS, Vol. 11372, Springer.
  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
  8. A True Positives Theorem for a Static Race Detector
    Proc. ACM Program. Lang. 2019. (POPL), ACM.
  9. Towards Mechanising Probabilistic Properties of a Blockchain
    Kiran Gopinathan, and Ilya Sergey
    CoqPL 2019. Informal Proceedings.

2018

  1. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale
    ACSAC 2018. ACM.
  2. RacerD: compositional static race detection
    Proc. ACM Program. Lang. 2018. (OOPSLA), ACM.
  3. Paxos Consensus, Deconstructed and Abstracted
    ESOP 2018. LNCS, Vol. 10801, Springer.
  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.
  6. Programming and Proving with Distributed Protocols
    Ilya Sergey, James R. Wilcox, and Zachary Tatlock
    Proc. ACM Program. Lang. 2018. (POPL), ACM.
  7. Scilla: a Smart Contract Intermediate-Level LAnguage
    Ilya Sergey, Amrit Kumar, and Aquinas Hobor
    CoRR 2018. Vol. abs/1801.00687, Technical Report.
  8. Automatic Inference of Gas Bounds for Smart Contracts on the Ethereum Blockchain
    2018. Unpublished draft.
    PDF

2017

  1. Modular, higher order cardinality analysis in theory and practice
    J. Funct. Program. 2017. Vol. 27, Cambridge University Press.
    PDF
  2. Concurrent Data Structures Linked in Time
    ECOOP 2017. LIPIcs, Vol. 74, Schloss Dagstuhl.
  3. A Concurrent Perspective on Smart Contracts
    Ilya Sergey, and Aquinas Hobor
    1st Workshop on Trusted Smart Contracts 2017. LNCS, Vol. 10323, Springer.
  4. Programming Language Abstractions for Modularly Verified Distributed Systems
    James R. Wilcox, Ilya Sergey, and Zachary Tatlock
    SNAPL 2017. LIPIcs, Vol. 71, Schloss Dagstuhl.

2016

  1. Hoare-Style Specifications as Correctness Conditions for Non-Linearizable Concurrent Objects
    OOPSLA 2016. ACM.
  2. Operational Aspects of C/C++ Concurrency
    CoRR 2016. Vol. abs/1606.01400, Working Draft.
  3. Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms
    Ilya Sergey
    ICFP 2016. ACM.

2015

  1. Mechanized Verification of Fine-Grained Concurrent Programs
    PLDI 2015. ACM.
  2. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
    ESOP 2015. LNCS, Vol. 9032, Springer.

2014

  1. Pushdown flow analysis with abstract garbage collection
    J. Funct. Program. 2014. Vol. 24, (2-3), Cambridge University Press.
    PDF
  2. Communicating State Transition Systems for Fine-Grained Concurrent Resources
    ESOP 2014. LNCS, Vol. 8410, Springer.
  3. Modular, Higher-Order Cardinality Analysis in Theory and Practice
    POPL 2014. ACM.
  4. Deriving Interpretations of the Gradually-Typed Lambda Calculus
    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
    PLDI 2013. ACM.
  2. Fixing Idioms: a Recursion Primitive for Applicative DSLs
    PEPM 2013. ACM.
  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.
  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),
  3. Gradual Ownership Types
    Ilya Sergey, and Dave Clarke
    ESOP 2012. LNCS, Vol. 7211, Springer.
  4. Introspective Pushdown Analysis of Higher-Order Programs
    ICFP 2012. ACM.
  5. Calculating Graph Algorithms for Dominance and Shortest Path
    Ilya Sergey, Jan Midtgaard, and Dave Clarke
    MPC 2012. LNCS, Vol. 7342, Springer.
  6. Theory and Practice of Demand Analysis in Haskell
    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.
  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
    The First Scala Workshop – Scala Days 2010. Informal Proceedings.
  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.

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.