Formal Specification and Verification of Smart Contracts for Azure Blockchain

Houdini, an annotation assistant for esc/java

Cormac Flanagan and K Rustan M Leino · 2001

Earlier work this paper cites.

Boogie: A modular reusable verifier for object-oriented programs

Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino · 2005

Earlier work this paper cites.

Efficient weakest preconditions

K. Rustan M. Leino · 2005

Earlier work this paper cites.

Complexity and algorithms for monomial and clausal predicate abstraction

Shuvendu Lahiri and Shaz Qadeer · 2009

Earlier work this paper cites.

Intra-module inference

Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, and Thomas Wies · 2009

Earlier work this paper cites.

A solver for reachability modulo theories

Akash Lal, Shaz Qadeer, and Shuvendu K. Lahiri · 2012

Earlier work this paper cites.

https://medium.com/\spacefactor\@m{}MyPaoG/explaining-the-dao-exploit-for-beginners-in-solidity-80ee84f0d470 , 2016

Explaining the dao exploit for beginners in solidity · 2016

Earlier work this paper cites.

https://solidity.readthedocs.io/en/v0.4.24/structure-of-a-contract.html#function-modifiers , 2016

Solidity: Function modifiers · 2016

Earlier work this paper cites.

Formal verification of smart contracts: Short paper

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella Béguelin · 2016

Earlier work this paper cites.

Making smart contracts smarter

Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor · 2016

Earlier work this paper cites.

https://azure.microsoft.com/en-us/solutions/blockchain/ , 2017

Azure blockchain · 2017

Cited alongside, same era.

https://www.theregister.co.uk/2017/11/16/parity_flaw_not_fixed , 2017

Parity: The bug that put $169m of ethereum on ice? yeah, it was on the todo list for months · 2017

Cited alongside, same era.

A survey of attacks on ethereum smart contracts (sok)

Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli · 2017

Cited alongside, same era.

https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples , 2018

Applications and smart contract samples for workbench · 2018

Cited alongside, same era.

https://github.com/Azure-Samples/blockchain , 2018

Azure blockchain content and samples · 2018

Cited alongside, same era.

https://azure.microsoft.com/en-us/features/blockchain-workbench/ , 2018

https://github.com/trailofbits/slither , 2018

Slither, the solidity source analyzer · 2018

Closest in time.

Madmax: surviving out-of-gas conditions in ethereum smart contracts

Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis · 2018

Closest in time.

Online detection of effectively callback free objects with applications to smart contracts

Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar · 2018

Closest in time.

KEVM: A complete formal semantics of the ethereum virtual machine

Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu · 2018

Closest in time.

ZEUS: analyzing safety of smart contracts

Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma · 2018

Closest in time.

Tool demonstration: Fsolidm for designing secure ethereum smart contracts