Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Thi Thu Ha Doan,
  • Peter Thiemann

摘要

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.