58 citations · 69 across the 7 of their papers we have counts for
9 papers · 1 filter
Compiling a Higher-Order Smart Contract Language to LLVM
Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov +3
Scilla is a higher-order polymorphic typed intermediate level language for implementing smart contracts. In this talk, we describe a Scilla compiler targeting LLVM, with a focus on…
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- Extended Version
Andreea Costea, Amy Zhu, Nadia Polikarpova +1
In program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if…
A True Positives Theorem for a Static Race Detector - Extended Version
Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
RacerD is a static race detector that has been proven to be effective in engineering practice: it has seen thousands of data races fixed by developers before reaching production, a…
Running on Fumes--Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis
Elvira Albert, Pablo Gordillo, Albert Rubio +1
Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction exec…
Structuring the Synthesis of Heap-Manipulating Programs - Extended Version
Nadia Polikarpova, Ilya Sergey
This paper describes a deductive approach to synthesizing imperative programs with pointers from declarative specifications expressed in Separation Logic. Our synthesis algorithm t…
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
Elvira Albert, Pablo Gordillo, Benjamin Livshits +2
Analyzing Ethereum bytecode, rather than the source code from which it was generated, is a necessity when: (1) the source code is not available (e.g., the blockchain only stores th…