Celestial: A Smart Contracts Verification Framework

Dharanikota, Samvid; Mukherjee, Suvam; Bhardwaj, Chandrika; Rastogi, Aseem; Lal, Akash

doi:10.34727/2021/isbn.978-3-85448-046-4_22

Record link:

http://hdl.handle.net/20.500.12708/18645
https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_22

Title:

Celestial: A Smart Contracts Verification Framework

Citation:

Dharanikota, S., Mukherjee, S., Bhardwaj, C., Rastogi, A., & Lal, A. (2021). Celestial: A Smart Contracts Verification Framework. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 133–142). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_22

reposiTUm DOI:

10.34727/2021/isbn.978-3-85448-046-4_22

CatalogPlus:

AC17204380

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Dharanikota, Samvid
Mukherjee, Suvam
Bhardwaj, Chandrika
Rastogi, Aseem
Lal, Akash

Organisational Unit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering

Series:

Conference Series: Formal Methods in Computer-Aided Design

Published in:

Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021

Date (published):

Oct-2021

Number of Pages:

Publisher:

TU Wien Academic Press, Wien

Peer reviewed:

Yes

Keywords:

smart contract; blockchain; reliability; testing

Abstract:

We present CELESTIAL, a framework for formally verifying smart contracts written in the Solidity language for the Ethereum blockchain. CELESTIAL allows programmers to write expressive functional specifications for their contracts. It translates the contracts and the specifications to F⋆ to formally verify, against an F⋆ model of the blockchain semantics, that the contracts meet their specificatio...

Linked records in reposiTUm: has part:

10.34727/2021/isbn.978-3-85448-046-4

License:

CC BY 4.0