research
∙
05/04/2023
Distributed System Fuzzing
Grey-box fuzzing is the lightweight approach of choice for finding bugs ...
share
research
∙
08/05/2021
HIPPODROME: Data Race Repair using Static Analysis Summaries
Implementing bug-free concurrent programs is a challenging task in moder...
research
∙
08/12/2020
Compiling a Higher-Order Smart Contract Language to LLVM
Scilla is a higher-order polymorphic typed intermediate level language f...
research
∙
04/28/2020
Certifying Certainty and Uncertainty in Approximate Membership Query Structures – Extended Version
Approximate Membership Query structures (AMQs) rely on randomisation for...
research
∙
03/13/2020
QED at Large: A Survey of Engineering of Formally Verified Software
Development of formal proofs of correctness of programs can increase act...
research
∙
01/29/2020
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers – Extended Version
In program synthesis there is a well-known trade-off between concise and...
research
∙
11/22/2018
GASTAP: A Gas Analyzer for Smart Contracts
Gas is a measurement unit of the computational effort that it will take ...
research
∙
11/08/2018
A True Positives Theorem for a Static Race Detector - Extended Version
RacerD is a static race detector that has been proven to be effective in...
research
∙
10/27/2018
Exploiting The Laws of Order in Smart Contracts
We investigate a family of bugs in blockchain-based smart contracts, whi...
research
∙
07/18/2018
Structuring the Synthesis of Heap-Manipulating Programs - Extended Version
This paper describes a deductive approach to synthesizing imperative pro...
research
∙
07/18/2018
Structuring the Synthesis of Heap-Manipulating Programs
This paper describes a deductive approach to synthesizing imperative pro...
research
∙
05/10/2018
EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
Analyzing Ethereum bytecode, rather than the source code from which it w...
research
∙
02/16/2018
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale
Smart contracts---stateful executable objects hosted on blockchains like...
research
∙
02/16/2018
Paxos Consensus, Deconstructed and Abstracted (Extended Version)
Lamport's Paxos algorithm is a classic consensus protocol for state mach...
research
∙
01/02/2018
Scilla: a Smart Contract Intermediate-Level LAnguage
This paper outlines key design principles of Scilla---an intermediate-le...
research
∙
06/19/2014