Google Scholar DBLP CSAuthors
2024
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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.