[Google Scholar] [DBLP] [CSAuthors]


  1. Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
    VMCAI 2021. To appear.
  2. Protocol Combinators for Modeling, Testing, and Execution of Distributed Systems
    J. Funct. Program. 2021. Cambridge University Press. To appear.


  1. Certifying Certainty and Uncertainty in Approximate Membership Query Structures
    Kiran Gopinathan, and Ilya Sergey
    CAV 2020. LNCS, Vol. 12225, Pages 279–303. 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, Pages 141–168. Springer.


  1. QED at Large: A Survey of Engineering of Formally Verified Software
    Found. Trends Program. Lang. 2019. Vol. 5, (2-3), Pages 102–281.
  2. Safer Smart Contract Programming with Scilla
    Proc. ACM Program. Lang. 2019. Vol. 3 (OOPSLA), Pages 185:1–185:30. ACM.
    OOPSLA 2019 Distinguished Artifact Award
  3. Exploiting the laws of order in smart contracts
    ISSTA 2019. Pages 363–373. ACM.
  4. Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis
    VECoS 2019. LNCS, Vol. 11847, Pages 63–78. Springer.
  5. Engineering Distributed Systems that We Can Trust (and Also Run)
    Ilya Sergey
    PODC 2019. ACM. Invited Talk.
  6. Distributed Protocol Combinators
    PADL 2019. LNCS, Vol. 11372, Pages 169–186. Springer.
  7. Structuring the Synthesis of Heap-Manipulating Programs
    Nadia Polikarpova, and Ilya Sergey
    Proc. ACM Program. Lang. 2019. Vol. 3 (POPL), Pages 72:1–72:30. ACM.
    POPL 2019 Distinguished Paper Award
  8. A True Positives Theorem for a Static Race Detector
    Proc. ACM Program. Lang. 2019. Vol. 3 (POPL), Pages 57:1–57:29. ACM.
  9. Towards Mechanising Probabilistic Properties of a Blockchain
    Kiran Gopinathan, and Ilya Sergey
    CoqPL 2019. Informal Proceedings.


  1. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale
    ACSAC 2018. Pages 653–663. ACM.
  2. RacerD: compositional static race detection
    Proc. ACM Program. Lang. 2018. Vol. 2 (OOPSLA), Pages 144:1–144:28. ACM.
  3. Paxos Consensus, Deconstructed and Abstracted
    ESOP 2018. LNCS, Vol. 10801, Pages 912–939. Springer.
  4. Temporal Properties of Smart Contracts
    Ilya Sergey, Amrit Kumar, and Aquinas Hobor
    ISoLA 2018. LNCS, Vol. 11247, Pages 323–338. Springer.
  5. Mechanising Blockchain Consensus
    George Pîrlea, and Ilya Sergey
    CPP 2018. Pages 78–90. ACM.
  6. Programming and Proving with Distributed Protocols
    Ilya Sergey, James R. Wilcox, and Zachary Tatlock
    Proc. ACM Program. Lang. 2018. Vol. 2 (POPL), Pages 28:1–28:30. 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.


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


  1. Hoare-Style Specifications as Correctness Conditions for Non-Linearizable Concurrent Objects
    OOPSLA 2016. Pages 92–110. 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. Pages 193–199. ACM.


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


  1. Pushdown flow analysis with abstract garbage collection
    J. Funct. Program. 2014. Vol. 24, (2-3), Pages 218–283. Cambridge University Press.
  2. Communicating State Transition Systems for Fine-Grained Concurrent Resources
    ESOP 2014. LNCS, Vol. 8410, Pages 290–310. Springer.
  3. Modular, Higher-Order Cardinality Analysis in Theory and Practice
    POPL 2014. Pages 335–348. ACM.
  4. Deriving Interpretations of the Gradually-Typed Lambda Calculus
    PEPM 2014. Pages 157–168. ACM.
  5. Introducing Functional Programmers to Interactive Theorem Proving and Program Verification
    Ilya Sergey, and Aleksandar Nanevski
    2014. Unpublished draft.


  1. Monadic abstract interpreters
    PLDI 2013. Pages 399–410. ACM.
  2. Fixing Idioms: a Recursion Primitive for Applicative DSLs
    PEPM 2013. Pages 97–106. 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, Pages 15–58. Springer.


  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), Pages 13–20.
  3. Gradual Ownership Types
    Ilya Sergey, and Dave Clarke
    ESOP 2012. LNCS, Vol. 7211, Pages 579–599. Springer.
  4. Introspective Pushdown Analysis of Higher-Order Programs
    ICFP 2012. Pages 177–188. ACM.
  5. Calculating Graph Algorithms for Dominance and Shortest Path
    Ilya Sergey, Jan Midtgaard, and Dave Clarke
    MPC 2012. LNCS, Vol. 7342, Pages 132–156. Springer.
  6. Theory and Practice of Demand Analysis in Haskell
    2012. Unpublished draft.


  1. From type checking by recursive descent to type checking with an abstract machine
    Ilya Sergey, and Dave Clarke
    LDTA 2011. Pages 2. ACM.
  2. Implementation of Gradual Ownership Types for Java using Attribute Grammars
    Ilya Sergey
    Software Engineering. 2011. Vol. 6, Pages 46-79. Saint Petersburg State University Publishing. In Russian.


  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.


  1. A Semantics for Context-Oriented Programming with Layers
    Dave Clarke, and Ilya Sergey
    First International Workshop on Context-Oriented Programming (COP) 2009. Pages 10:1–10:6. ACM.


  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.
  2. Extraction of Musical Notation from a Musical Signal
    Ilya Sergey
    MSc Thesis. Saint Petersburg State University, Russia. 2008. In Russian.