Ilya Sergey
Person information
- affiliation: 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
2010 – today
- 2019
- [j9]Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock:
QED at Large: A Survey of Engineering of Formally Verified Software. Foundations and Trends in Programming Languages 5(2-3): 102-281 (2019) - [j8]Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, Ken Chan Guan Hao:
Safer smart contract programming with Scilla. PACMPL 3(OOPSLA): 185:1-185:30 (2019) - [j7]Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
:
A true positives theorem for a static race detector. PACMPL 3(POPL): 57:1-57:29 (2019) - [j6]Nadia Polikarpova, Ilya Sergey
:
Structuring the synthesis of heap-manipulating programs. PACMPL 3(POPL): 72:1-72:30 (2019) - [c26]Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena:
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, Albert Rubio, Ilya Sergey:
Running on Fumes - Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. VECoS 2019: 63-78 - 2018
- [j5]Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
:
RacerD: compositional static race detection. PACMPL 2(OOPSLA): 144:1-144:28 (2018) - [j4]Ilya Sergey
, James R. Wilcox, Zachary Tatlock:
Programming and proving with distributed protocols. PACMPL 2(POPL): 28:1-28:30 (2018) - [c22]Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor:
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. ACSAC 2018: 653-663 - [c21]Elvira Albert, Pablo Gordillo
, Benjamin Livshits, Albert Rubio, Ilya Sergey:
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. ATVA 2018: 513-520 - [c20]George Pîrlea, Ilya Sergey
:
Mechanising blockchain consensus. CPP 2018: 78-90 - [c19]Álvaro García-Pérez
, Alexey Gotsman, Yuri Meshman, Ilya Sergey
:
Paxos Consensus, Deconstructed and Abstracted. ESOP 2018: 912-939 - [c18]Ilya Sergey, Amrit Kumar, Aquinas Hobor:
Temporal Properties of Smart Contracts. ISoLA (4) 2018: 323-338 - [i15]Ilya Sergey
, Amrit Kumar, Aquinas Hobor:
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
, Prateek Saxena, Aquinas Hobor:
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, Albert Rubio, Ilya Sergey:
GASTAP: A Gas Analyzer for Smart Contracts. CoRR abs/1811.10403 (2018) - 2017
- [d1]Germán Andrés Delbianco
, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Concurrent Data Structures Linked in Time (Artifact). DARTS 3(2): 04:1-04:4 (2017) - [j3]Ilya Sergey
, Dimitrios Vytiniotis, Simon L. Peyton Jones, Joachim Breitner:
Modular, higher order cardinality analysis in theory and practice. J. Funct. Program. 27: e11 (2017) - [c17]Germán Andrés Delbianco
, Ilya Sergey
, Aleksandar Nanevski, Anindya Banerjee:
Concurrent Data Structures Linked in Time. ECOOP 2017: 8:1-8:30 - [c16]Ilya Sergey
, Aquinas Hobor:
A Concurrent Perspective on Smart Contracts. Financial Cryptography Workshops 2017: 478-493 - [c15]James R. Wilcox, Ilya Sergey
, Zachary Tatlock:
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
, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
:
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
, Aleksandar Nanevski:
Operational Aspects of C/C++ Concurrency. CoRR abs/1606.01400 (2016) - 2015
- [c12]Ilya Sergey
, Aleksandar Nanevski, Anindya Banerjee:
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP 2015: 333-358 - [c11]Ilya Sergey
, Aleksandar Nanevski, Anindya Banerjee:
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]J. Ian Johnson, Ilya Sergey
, Christopher Earl, Matthew Might, David Van Horn:
Pushdown flow analysis with abstract garbage collection. J. Funct. Program. 24(2-3): 218-283 (2014) - [c10]Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey
, Germán Andrés Delbianco
:
Communicating State Transition Systems for Fine-Grained Concurrent Resources. ESOP 2014: 290-310 - [c9]Álvaro García-Pérez
, Pablo Nogueira, Ilya Sergey
:
Deriving interpretations of the gradually-typed lambda calculus. PEPM 2014: 157-168 - [c8]Ilya Sergey
, Dimitrios Vytiniotis, Simon L. Peyton Jones:
Modular, higher-order cardinality analysis in theory and practice. POPL 2014: 335-348 - [i3]J. Ian Johnson, 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
, Ilya Sergey
, Dave Clarke, Frank Piessens:
Fixing idioms: a recursion primitive for applicative DSLs. PEPM 2013: 97-106 - [c6]Ilya Sergey
, Dominique Devriese
, Matthew Might, Jan Midtgaard
, David Darais, Dave Clarke, Frank Piessens:
Monadic abstract interpreters. PLDI 2013: 399-410 - [p1]Dave Clarke, Johan Östlund, Ilya Sergey
, Tobias Wrigstad:
Ownership Types: A Survey. Aliasing in Object-Oriented Programming 2013: 15-58 - 2012
- [j1]Ilya Sergey
, Dave Clarke:
A correspondence between type checking via reduction and type checking via evaluation. Inf. Process. Lett. 112(1-2): 13-20 (2012) - [c5]Ilya Sergey
, Dave Clarke:
Gradual Ownership Types. ESOP 2012: 579-599 - [c4]Christopher Earl, Ilya Sergey
, Matthew Might, David Van Horn:
Introspective pushdown analysis of higher-order programs. ICFP 2012: 177-188 - [c3]Ilya Sergey
, Jan Midtgaard
, Dave Clarke:
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
, Dave Clarke:
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).
load content from web.archive.org
Privacy notice: By enabling the option above, your browser will contact the API of web.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 and opencitations.net 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 Crossref privacy policy and the OpenCitations privacy policy.
Citation data
Add a list of citing articles from 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 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.
Tweets on dblp homepage
Show tweets from on the dblp homepage.
Privacy notice: By enabling the option above, your browser will contact twitter.com and twimg.com to load tweets curated by our Twitter accout. At the same time, Twitter will persitently store several cookies with your web browser. While we did signal Twitter to not track our users by setting the "dnt" flag, we do not have any control over how Twitter uses your data. So please proceed with care and consider checking the Twitter privacy policy.
last updated on 2019-11-14 23:07 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint