Google Scholar
DBLP
CSAuthors
2024
Mechanised Hypersafety Proofs about Structured Data
Proc. ACM Program. Lang.
2024.
Vol. 8,
(PLDI),
Pages 173:1–173:24.
ACM.
Small Scale Reflection for the Working Lean User
2024.
In submission.
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
CPP
2024.
Pages 45-59.
ACM.
Distinguished Paper Award
2023
Greybox Fuzzing of Distributed Systems
30th ACM Conference on Computer and Communications Security (CCS)
2023.
Pages 1615-1629.
ACM.
Adventure of a Lifetime: Extract Method Refactoring for Rust
Proc. ACM Program. Lang.
2023.
Vol. 7,
(OOPSLA),
Pages 245:1–245:28.
ACM.
Mostly Automated Proof Repair for Verified Libraries
Proc. ACM Program. Lang.
2023.
Vol. 7,
(PLDI),
Pages 107:1–107:25.
ACM.
ACM SIGPLAN Distinguished Paper Award
Leveraging Rust Types for Program Synthesis
Proc. ACM Program. Lang.
2023.
Vol. 7,
(PLDI),
Pages 164:1–164:24.
ACM.
Distinguished Artifact Award
Hippodrome: Data Race Repair using Static Analysis Summaries
ACM Trans. Softw. Eng. Methodol.
2023.
Vol. 32,
(2),
Pages 41:1–41:33.
ACM.
2022
Random Testing of a Higher-Order Blockchain Language (Experience Report)
Proc. ACM Program. Lang.
2022.
Vol. 6,
(ICFP),
Pages 122:1–122:16.
ACM.
2021
Certifying the Synthesis of Heap-Manipulating Programs
Proc. ACM Program. Lang.
2021.
Vol. 5,
(ICFP),
Pages 84:1–84:29.
ACM.
The Next 700 Smart Contract Languages
Ilya Sergey
Principles of Blockchain Systems
2021.
Pages 69–94.
Morgan & Claypool.
Author’s version.
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities (Invited Paper)
CAV
2021.
LNCS,
Vol. 12759,
Pages 110–134.
Springer.
Cyclic Program Synthesis
PLDI
2021.
Pages 944–959.
ACM.
ACM SIGPLAN Distinguished Paper Award
Practical Smart Contract Sharding with Ownership and Commutativity Analysis
PLDI
2021.
Pages 1327–1341.
ACM.
Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis
VMCAI
2021.
LNCS,
Vol. 12597,
Pages 376–400.
Springer.
Protocol Combinators for Modeling, Testing, and Execution of Distributed Systems
J. Funct. Program.
2021.
Vol. 31,
Cambridge University Press.
2020
Certifying Certainty and Uncertainty in Approximate Membership Query
Structures
CAV
2020.
LNCS,
Vol. 12225,
Pages 279–303.
Springer.
Compiling a Higher-Order Smart Contract Language to LLVM
CoRR
2020.
Accepted to 2020 Virtual LLVM Developers Meeting.
Concise Read-Only Specifications for Better Synthesis of Programs
with Pointers
ESOP
2020.
LNCS,
Vol. 12075,
Pages 141–168.
Springer.
2019
QED at Large: A Survey of Engineering of Formally Verified Software
Found. Trends Program. Lang.
2019.
Vol. 5,
(2-3),
Pages 102–281.
Safer Smart Contract Programming with Scilla
Proc. ACM Program. Lang.
2019.
Vol. 3,
(OOPSLA),
Pages 185:1–185:30.
ACM.
Distinguished Artifact Award
Exploiting the laws of order in smart contracts
ISSTA
2019.
Pages 363–373.
ACM.
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.
Engineering Distributed Systems that We Can Trust (and Also Run)
Ilya Sergey
PODC
2019.
ACM.
Invited Talk.
Distributed Protocol Combinators
PADL
2019.
LNCS,
Vol. 11372,
Pages 169–186.
Springer.
Structuring the Synthesis of Heap-Manipulating Programs
Proc. ACM Program. Lang.
2019.
Vol. 3
(POPL),
Pages 72:1–72:30.
ACM.
ACM SIGPLAN Distinguished Paper Award
A True Positives Theorem for a Static Race Detector
Proc. ACM Program. Lang.
2019.
Vol. 3
(POPL),
Pages 57:1–57:29.
ACM.
Towards Mechanising Probabilistic Properties of a Blockchain
CoqPL
2019.
Informal Proceedings.
2018
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale
ACSAC
2018.
Pages 653–663.
ACM.
RacerD: compositional static race detection
Proc. ACM Program. Lang.
2018.
Vol. 2
(OOPSLA),
Pages 144:1–144:28.
ACM.
Paxos Consensus, Deconstructed and Abstracted
ESOP
2018.
LNCS,
Vol. 10801,
Pages 912–939.
Springer.
Temporal Properties of Smart Contracts
ISoLA
2018.
LNCS,
Vol. 11247,
Pages 323–338.
Springer.
Mechanising Blockchain Consensus
CPP
2018.
Pages 78–90.
ACM.
Programming and Proving with Distributed Protocols
Proc. ACM Program. Lang.
2018.
Vol. 2
(POPL),
Pages 28:1–28:30.
ACM.
Scilla: a Smart Contract Intermediate-Level LAnguage
CoRR
2018.
Vol. abs/1801.00687,
Technical Report.
Automatic Inference of Gas Bounds for Smart Contracts on the Ethereum Blockchain
2018.
Unpublished draft.
2017
Modular, higher order cardinality analysis in theory and practice
J. Funct. Program.
2017.
Vol. 27,
Cambridge University Press.
Concurrent Data Structures Linked in Time
ECOOP
2017.
LIPIcs,
Vol. 74,
Pages 8:1–8:30.
Schloss Dagstuhl.
A Concurrent Perspective on Smart Contracts
1st Workshop on Trusted Smart Contracts
2017.
LNCS,
Vol. 10323,
Pages 478–493.
Springer.
Programming Language Abstractions for Modularly Verified Distributed
Systems
SNAPL
2017.
LIPIcs,
Vol. 71,
Pages 19:1–19:12.
Schloss Dagstuhl.
2016
Hoare-Style Specifications as Correctness Conditions for Non-Linearizable
Concurrent Objects
OOPSLA
2016.
Pages 92–110.
ACM.
Operational Aspects of C/C++ Concurrency
CoRR
2016.
Vol. abs/1606.01400,
Working Draft.
Experience Report: Growing and Shrinking Polygons for Random Testing
of Computational Geometry Algorithms
Ilya Sergey
ICFP
2016.
Pages 193–199.
ACM.
2015
Mechanized Verification of Fine-Grained Concurrent Programs
PLDI
2015.
Pages 77–87.
ACM.
Specifying and Verifying Concurrent Algorithms with Histories and
Subjectivity
ESOP
2015.
LNCS,
Vol. 9032,
Pages 333–358.
Springer.
2014
Pushdown flow analysis with abstract garbage collection
J. Funct. Program.
2014.
Vol. 24,
(2-3),
Pages 218–283.
Cambridge University Press.
Communicating State Transition Systems for Fine-Grained Concurrent
Resources
ESOP
2014.
LNCS,
Vol. 8410,
Pages 290–310.
Springer.
Modular, Higher-Order Cardinality Analysis in Theory and Practice
POPL
2014.
Pages 335–348.
ACM.
Deriving Interpretations of the Gradually-Typed Lambda Calculus
PEPM
2014.
Pages 157–168.
ACM.
Introducing Functional Programmers to Interactive Theorem
Proving and Program Verification
2014.
Unpublished draft.
2013
Monadic abstract interpreters
PLDI
2013.
Pages 399–410.
ACM.
Fixing Idioms: a Recursion Primitive for Applicative DSLs
PEPM
2013.
Pages 97–106.
ACM.
Ownership Types: A Survey
Aliasing in Object-Oriented Programming. Types, Analysis and Verification
2013.
LNCS,
Vol. 7850,
Pages 15–58.
Springer.
2012
Operational Aspects of Type Systems
Ilya Sergey
PhD Thesis.
KU Leuven, Leuven, Belgium.
2012.
A correspondence between type checking via reduction and type checking
via evaluation
Inf. Process. Lett.
2012.
Vol. 112,
(1-2),
Pages 13–20.
Gradual Ownership Types
ESOP
2012.
LNCS,
Vol. 7211,
Pages 579–599.
Springer.
Introspective Pushdown Analysis of Higher-Order Programs
ICFP
2012.
Pages 177–188.
ACM.
Calculating Graph Algorithms for Dominance and Shortest Path
MPC
2012.
LNCS,
Vol. 7342,
Pages 132–156.
Springer.
Theory and Practice of Demand Analysis in Haskell
2012.
Unpublished draft.
2011
From type checking by recursive descent to type checking with an abstract
machine
LDTA
2011.
Pages 2.
ACM.
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.
2010
Automatic refactorings for Scala programs
The First Scala Workshop – Scala Days
2010.
Informal Proceedings.
Scripting an IDE for EDSL Awareness
2010.
Unpublished draft.
2009
A Semantics for Context-Oriented Programming with Layers
First International Workshop on Context-Oriented
Programming (COP)
2009.
Pages 10:1–10:6.
ACM.
2008
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.
Extraction of Musical Notation from a Musical Signal
Ilya Sergey
MSc Thesis.
Saint Petersburg State University, Russia.
2008.
In Russian.