A Concurrent Perspective on Smart Contracts

The existence of refinement mappings

M. Abadi and L. Lamport · 1988

Earlier work this paper cites.

Linearizability: A correctness condition for concurrent objects

M. Herlihy and J. M. Wing · 1990

Earlier work this paper cites.

Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers

L. Lamport · 2002

Earlier work this paper cites.

Permission accounting in separation logic

R. Bornat, C. Calcagno, P. W. O’Hearn, and M. J. Parkinson · 2005

Earlier work this paper cites.

Java Concurrency in Practice

B. Goetz, T. Peierls, J. Bloch, J. Bowbeer, D. Holmes, and D. Lea · 2006

Earlier work this paper cites.

Resources, concurrency, and local reasoning

P. W. O’Hearn · 2007

Earlier work this paper cites.

The art of multiprocessor programming

M. Herlihy and N. Shavit · 2008

Earlier work this paper cites.

Proving that non-blocking algorithms don’t block

A. Gotsman, B. Cook, M. J. Parkinson, and V. Vafeiadis · 2009

Earlier work this paper cites.

Understanding and effectively preventing the aba problem in descriptor-based lock-free designs

D. Dechev, P. Pirkelbauer, and B. Stroustrup · 2010

Earlier work this paper cites.

Concurrent Abstract Predicates

T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis · 2010

Earlier work this paper cites.

Flat combining and the synchronization-parallelism tradeoff

D. Hendler, I. Incze, N. Shavit, and M. Tzafrir · 2010

Earlier work this paper cites.

Secure distributed programming with value-dependent types

N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan, and J. Yang · 2011

Earlier work this paper cites.

Programming and reasoning with algebraic effects and dependent types

E. Brady · 2013

Cited alongside, same era.

Why3 - Where Programs Meet Provers

J. Filliâtre and A. Paskevich · 2013

Cited alongside, same era.

CHECK-THEN-ACT misuse of java concurrent collections

Y. Lin and D. Dig · 2013

Cited alongside, same era.

Modular reasoning about separation of concurrent data structures

K. Svendsen, L. Birkedal, and M. J. Parkinson · 2013

Cited alongside, same era.

Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency

A. Turon, D. Dreyer, and L. Birkedal · 2013

Cited alongside, same era.

Lem: reusable engineering of real-world semantics

D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell · 2014

Cited alongside, same era.

Concurrent separation logic

S. Brookes and P. W. O’Hearn · 2016

Later among the works it cites.

Critical Update Re: DAO Vulnerability

V. Buterin · 2016

Later among the works it cites.

Symbolic abstract data type inference

M. Emmi and C. Enea · 2016

Later among the works it cites.

The DAO, 2016

C. Jentzsch · 2016

Later among the works it cites.

A program logic for concurrent objects under fair scheduling

H. Liang and X. Feng · 2016

Later among the works it cites.

Making smart contracts smarter

L. Luu, D. Chu, H. Olickel, P. Saxena, and A. Hobor · 2016

Later among the works it cites.

Safer Smart Contracts through Type-Driven Development

J. Pettersson and R. Edström · 2016