default search action
Ilya Sergey
Person information
- affiliation: School of Computing, National University of Singapore
- affiliation (former): University College London, Department of Computer Science, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j20]David Young, Ziyi Yang, Ilya Sergey, Alex Potanin:
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact). Dagstuhl Artifacts Ser. 10(2): 25:1-25:2 (2024) - [j19]Callista Le
, Kiran Gopinathan
Concurrent Data Structures Made Easy. Proc. ACM Program. Lang. 8(OOPSLA2): 1814-1842 (2024) - [j18]Vladimir Gladshtein
Mechanised Hypersafety Proofs about Structured Data. Proc. ACM Program. Lang. 8(PLDI): 647-670 (2024) - [c36]Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, Ilya Sergey:
Compositional Verification of Composite Byzantine Protocols. CCS 2024: 34-48 - [c35]Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. CPP 2024: 45-59 - [c34]David Young, Ziyi Yang, Ilya Sergey, Alex Potanin:
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers. ECOOP 2024: 45:1-45:26 - [i26]Vladimir Gladshtein, George Pîrlea, Ilya Sergey:
Small Scale Reflection for the Working Lean User. CoRR abs/2403.12733 (2024) - [i25]Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman P. Amarasinghe, Ilya Sergey:
Mechanised Hypersafety Proofs about Structured Data: Extended Version. CoRR abs/2404.06477 (2024) - [i24]David Young, Ziyi Yang, Ilya Sergey, Alex Potanin:
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version). CoRR abs/2407.09143 (2024) - [i23]Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, Ilya Sergey:
Concurrent Data Structures Made Easy (Extended Version). CoRR abs/2408.13779 (2024) - 2023
- [j17]Sewen Thy
Adventure of a Lifetime: Extract Method Refactoring for Rust. Proc. ACM Program. Lang. 7(OOPSLA2): 658-685 (2023) - [j16]Kiran Gopinathan
Mostly Automated Proof Repair for Verified Libraries. Proc. ACM Program. Lang. 7(PLDI): 25-49 (2023) - [j15]Jonás Fiala
Leveraging Rust Types for Program Synthesis. Proc. ACM Program. Lang. 7(PLDI): 1414-1437 (2023) - [j14]Andreea Costea
Hippodrome: Data Race Repair Using Static Analysis Summaries. ACM Trans. Softw. Eng. Methodol. 32(2): 41:1-41:33 (2023) - [c33]Ruijie Meng
Greybox Fuzzing of Distributed Systems. CCS 2023: 1615-1629 - [e3]Martin Gebser
Practical Aspects of Declarative Languages - 26th International Symposium, PADL 2024, London, UK, January 15-16, 2024, Proceedings. Lecture Notes in Computer Science 14512, Springer 2023, ISBN 978-3-031-52037-2 [contents] - [i22]Ruijie Meng, George Pîrlea, Abhik Roychoudhury, Ilya Sergey:
Distributed System Fuzzing. CoRR abs/2305.02601 (2023) - [i21]Swen Jacobs, Kenneth L. McMillan, Roopsha Samanta, Ilya Sergey:
Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112). Dagstuhl Reports 13(3): 32-48 (2023) - 2022
- [j13]Tram Hoang
Random testing of a higher-order blockchain language (experience report). Proc. ACM Program. Lang. 6(ICFP): 886-901 (2022) - [e2]Ilya Sergey
Programming Languages and Systems - 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings. Lecture Notes in Computer Science 13658, Springer 2022, ISBN 978-3-031-21036-5 [contents] - [e1]Ilya Sergey
Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings. Lecture Notes in Computer Science 13240, Springer 2022, ISBN 978-3-030-99335-1 [contents] - 2021
- [j12]Kristoffer Just Arndal Andersen
Protocol combinators for modeling, testing, and execution of distributed systems. J. Funct. Program. 31: e3 (2021) - [j11]Yasunari Watanabe, Kiran Gopinathan, George Pîrlea
Certifying the synthesis of heap-manipulating programs. Proc. ACM Program. Lang. 5(ICFP): 1-29 (2021) - [c32]Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper). CAV (1) 2021: 110-134 - [c31]Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe
Cyclic program synthesis. PLDI 2021: 944-959 - [c30]George Pîrlea
Practical smart contract sharding with ownership and commutativity analysis. PLDI 2021: 1327-1341 - [c29]Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin:
Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis. VMCAI 2021: 376-400 - [i20]Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, Ilya Sergey:
HIPPODROME: Data Race Repair using Static Analysis Summaries. CoRR abs/2108.02490 (2021) - 2020
- [c28]Kiran Gopinathan
Certifying Certainty and Uncertainty in Approximate Membership Query Structures. CAV (2) 2020: 279-303 - [c27]Andreea Costea
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers. ESOP 2020: 141-168 - [i19]Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey:
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers - Extended Version. CoRR abs/2001.10723 (2020) - [i18]Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock:
QED at Large: A Survey of Engineering of Formally Verified Software. CoRR abs/2003.06458 (2020) - [i17]Kiran Gopinathan, Ilya Sergey:
Certifying Certainty and Uncertainty in Approximate Membership Query Structures - Extended Version. CoRR abs/2004.13312 (2020) - [i16]Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pîrlea, Amrit Kumar, Ilya Sergey:
Compiling a Higher-Order Smart Contract Language to LLVM. CoRR abs/2008.05555 (2020)
2010 – 2019
- 2019
- [j10]Talia Ringer, Karl Palmskog, Ilya Sergey
QED at Large: A Survey of Engineering of Formally Verified Software. Found. Trends Program. Lang. 5(2-3): 102-281 (2019) - [j9]Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, Ken Chan Guan Hao:
Safer smart contract programming with Scilla. Proc. ACM Program. Lang. 3(OOPSLA): 185:1-185:30 (2019) - [j8]Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
A true positives theorem for a static race detector. Proc. ACM Program. Lang. 3(POPL): 57:1-57:29 (2019) - [j7]Nadia Polikarpova, Ilya Sergey
Structuring the synthesis of heap-manipulating programs. Proc. ACM Program. Lang. 3(POPL): 72:1-72:30 (2019) - [c26]Aashish Kolluri, Ivica Nikolic, Ilya Sergey
Exploiting the laws of order in smart contracts. ISSTA 2019: 363-373 - [c25]Kristoffer Just Arndal Andersen, Ilya Sergey
Distributed Protocol Combinators. PADL 2019: 169-186 - [c24]Ilya Sergey:
Engineering Distributed Systems that We Can Trust (and Also Run). PODC 2019: 306 - [c23]Elvira Albert, Pablo Gordillo
Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. VECoS 2019: 63-78 - 2018
- [j6]Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
RacerD: compositional static race detection. Proc. ACM Program. Lang. 2(OOPSLA): 144:1-144:28 (2018) - [j5]Ilya Sergey
Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2(POPL): 28:1-28:30 (2018) - [c22]Ivica Nikolic, Aashish Kolluri, Ilya Sergey
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. ACSAC 2018: 653-663 - [c21]Elvira Albert, Pablo Gordillo
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. ATVA 2018: 513-520 - [c20]George Pîrlea
Mechanising blockchain consensus. CPP 2018: 78-90 - [c19]Álvaro García-Pérez
Paxos Consensus, Deconstructed and Abstracted. ESOP 2018: 912-939 - [c18]Ilya Sergey
Temporal Properties of Smart Contracts. ISoLA (4) 2018: 323-338 - [i15]Ilya Sergey
Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR abs/1801.00687 (2018) - [i14]Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey:
Paxos Consensus, Deconstructed and Abstracted (Extended Version). CoRR abs/1802.05969 (2018) - [i13]Ivica Nikolic, Aashish Kolluri, Ilya Sergey
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. CoRR abs/1802.06038 (2018) - [i12]Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey:
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. CoRR abs/1805.07208 (2018) - [i11]Nadia Polikarpova, Ilya Sergey:
Structuring the Synthesis of Heap-Manipulating Programs. CoRR abs/1807.07022 (2018) - [i10]Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena:
Exploiting The Laws of Order in Smart Contracts. CoRR abs/1810.11605 (2018) - [i9]Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey:
A True Positives Theorem for a Static Race Detector - Extended Version. CoRR abs/1811.03503 (2018) - [i8]Elvira Albert, Pablo Gordillo
GASTAP: A Gas Analyzer for Smart Contracts. CoRR abs/1811.10403 (2018) - 2017
- [j4]Germán Andrés Delbianco
Concurrent Data Structures Linked in Time (Artifact). Dagstuhl Artifacts Ser. 3(2): 04:1-04:4 (2017) - [j3]Ilya Sergey
Modular, higher order cardinality analysis in theory and practice. J. Funct. Program. 27: e11 (2017) - [c17]Germán Andrés Delbianco
Concurrent Data Structures Linked in Time. ECOOP 2017: 8:1-8:30 - [c16]Ilya Sergey
A Concurrent Perspective on Smart Contracts. Financial Cryptography Workshops 2017: 478-493 - [c15]James R. Wilcox, Ilya Sergey
Programming Language Abstractions for Modularly Verified Distributed Systems. SNAPL 2017: 19:1-19:12 - [i7]Ilya Sergey, Aquinas Hobor:
A Concurrent Perspective on Smart Contracts. CoRR abs/1702.05511 (2017) - 2016
- [c14]Ilya Sergey
Experience report: growing and shrinking polygons for random testing of computational geometry algorithms. ICFP 2016: 193-199 - [c13]Ilya Sergey
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. OOPSLA 2016: 92-110 - [i6]Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Concurrent Data Structures Linked in Time. CoRR abs/1604.08080 (2016) - [i5]Anton Podkopaev, Ilya Sergey
Operational Aspects of C/C++ Concurrency. CoRR abs/1606.01400 (2016) - 2015
- [c12]Ilya Sergey
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP 2015: 333-358 - [c11]Ilya Sergey
Mechanized verification of fine-grained concurrent programs. PLDI 2015: 77-87 - [i4]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco:
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects. CoRR abs/1509.06220 (2015) - 2014
- [j2]Dionna Amalie Glaze, Ilya Sergey
Pushdown flow analysis with abstract garbage collection. J. Funct. Program. 24(2-3): 218-283 (2014) - [c10]Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey
Communicating State Transition Systems for Fine-Grained Concurrent Resources. ESOP 2014: 290-310 - [c9]Álvaro García-Pérez
Deriving interpretations of the gradually-typed lambda calculus. PEPM 2014: 157-168 - [c8]Ilya Sergey
Modular, higher-order cardinality analysis in theory and practice. POPL 2014: 335-348 - [i3]Dionna Amalie Glaze, Ilya Sergey, Christopher Earl, Matthew Might, David Van Horn:
Pushdown flow analysis with abstract garbage collection. CoRR abs/1406.5106 (2014) - [i2]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. CoRR abs/1410.0306 (2014) - 2013
- [c7]Dominique Devriese
Fixing idioms: a recursion primitive for applicative DSLs. PEPM 2013: 97-106 - [c6]Ilya Sergey
Monadic abstract interpreters. PLDI 2013: 399-410 - [p1]Dave Clarke, Johan Östlund, Ilya Sergey
Ownership Types: A Survey. Aliasing in Object-Oriented Programming 2013: 15-58 - 2012
- [j1]Ilya Sergey
A correspondence between type checking via reduction and type checking via evaluation. Inf. Process. Lett. 112(1-2): 13-20 (2012) - [c5]Ilya Sergey
Gradual Ownership Types. ESOP 2012: 579-599 - [c4]Christopher Earl, Ilya Sergey
Introspective pushdown analysis of higher-order programs. ICFP 2012: 177-188 - [c3]Ilya Sergey
Calculating Graph Algorithms for Dominance and Shortest Path. MPC 2012: 132-156 - [i1]Christopher Earl, Ilya Sergey, Matthew Might, David Van Horn:
Introspective Pushdown Analysis of Higher-Order Programs. CoRR abs/1207.1813 (2012) - 2011
- [c2]Ilya Sergey
From type checking by recursive descent to type checking with an abstract machine. LDTA 2011: 2
2000 – 2009
- 2009
- [c1]Dave Clarke, Ilya Sergey
A semantics for context-oriented programming with layers. COP@ECOOP 2009: 10:1-10:6
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-11 20:40 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: