A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution (APLAS 2024 - The 22nd Asian Symposium on Programming Languages and Systems)

Who

Thi Thu Ha Doan, Peter Thiemann

Track

APLAS 2024 Research Papers

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Thu 24 Oct 2024 14:30 - 15:00 at Yamauchi Hall - Verification Chair(s): Yuting Wang

Abstract

We developed SCV, a verification tool geared towards contracts implemented in Michelson, the smart contract language of the Tezos blockchain. SCV utilizes symbolic execution to derive verification conditions that can be checked automatically against user specifications using an SMT solver. These specifications are written in a domain-specific language. We present the fundamental principles behind the design and development of SCV. By pruning states during symbolic execution, SCV effectively addresses the problem of state explosion. This approach has enabled us to conduct two case studies on real-life contracts, demonstrating the expressiveness of our tool.

Thi Thu Ha Doan

University of Freiburg

Peter Thiemann

University of Freiburg, Germany