We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.SE

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Software Engineering

Title: Safety Verification of Declarative Smart Contracts

Abstract: Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is therefore an important task. This paper presents a safety verification tool DCV that targets declarative smart contracts written in DeCon, a logic-based domain-specific language for smart contract implementation and specification. DCV is sound and fully automatic. It proves safety properties by mathematical induction and can automatically infer inductive invariants without annotations from the developer. Our evaluation shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.
Comments: In submission to TACAS'23
Subjects: Software Engineering (cs.SE)
Cite as: arXiv:2211.14585 [cs.SE]
  (or arXiv:2211.14585v1 [cs.SE] for this version)

Submission history

From: Haoxian Chen [view email]
[v1] Sat, 26 Nov 2022 15:02:37 GMT (436kb,D)

Link back to: arXiv, form interface, contact.