publications

Google Scholar DBLP CSAuthors

2024

  1. 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
  2. Mechanised Hypersafety Proofs about Structured Data
    Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey
    Proc. ACM Program. Lang. 2024. Vol. 8, (PLDI), ACM.
    PDF arXiv Code Artifact
  3. Small Scale Reflection for the Working Lean User
    Vladimir Gladshtein, George Pîrlea, and Ilya Sergey
    2024. Unpublished draft.
    arXiv Code Artifact
  4. 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) 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. Vol. 7, (OOPSLA), ACM.
    PDF Artifact
  3. Mostly Automated Proof Repair for Verified Libraries
    Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey
    Proc. ACM Program. Lang. 2023. Vol. 7, (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. Vol. 7, (PLDI), ACM.
    Distinguished Artifact Award
    PDF Extended Version Artifact Slides Video
  5. 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. Vol. 6, (ICFP), ACM.
    PDF Artifact 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. Vol. 5, (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. Vol. 3, (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. Vol. 3 (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. Vol. 3 (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. Vol. 2 (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. Vol. 2 (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