activity
20172022
most citedScilla: a Smart Contract Intermediate-Level LAnguage

58 citations · 67 across the 3 of their papers we have counts for

collaborators

8 papers

cs.DC20221 cited

OverChain: Building a robust overlay with a blockchain

Vijeth Aradhya, Seth Gilbert, Aquinas Hobor

Blockchains use peer-to-peer networks for disseminating information among peers, but these networks currently do not have any provable guarantees for desirable properties such as B…

cs.LO2020

Complexity Analysis of Tree Share Structure

Xuan-Bach Le, Aquinas Hobor, Anthony W. Lin

The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are…

cs.PL2019

Proof Pearl: Magic Wand as Frame

Qinxiang Cao, Shengyi Wang, Aquinas Hobor +1

Separation logic adds two connectives to assertion languages: separating conjunction * ("star") and its adjoint, separating implication -* ("magic wand"). Comparatively, separating…

cs.CR2018

Exploiting The Laws of Order in Smart Contracts

Aashish Kolluri, Ivica Nikolic, Ilya Sergey +2

We investigate a family of bugs in blockchain-based smart contracts, which we call event-ordering (or EO) bugs. These bugs are intimately related to the dynamic ordering of contrac…

cs.CR2018

BesFS: A POSIX Filesystem for Enclaves with a Mechanized Safety Proof

Shweta Shinde, Shengyi Wang, Pinghai Yuan +3

New trusted computing primitives such as Intel SGX have shown the feasibility of running user-level applications in enclaves on a commodity trusted processor without trusting a lar…

cs.CR2018

Finding The Greedy, Prodigal, and Suicidal Contracts at Scale

Ivica Nikolic, Aashish Kolluri, Ilya Sergey +2

Smart contracts---stateful executable objects hosted on blockchains like Ethereum---carry billions of dollars worth of coins and cannot be updated once deployed. We present a new s…