A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson
No abstract available.
Related papers
- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types TACAS 2021
- Cost Analysis of Smart Contracts Via Parametric Resource Analysis SAS 2020
- A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution APLAS 2024
- SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models OOPSLA 2026
- DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance OOPSLA 2025
- MadMax: surviving out-of-gas conditions in Ethereum smart contracts OOPSLA 2018
- Symbolic value-flow static analysis: deep, precise, complete modeling of Ethereum smart contracts OOPSLA 2021
- Towards verifying ethereum smart contract bytecode in Isabelle/HOL CPP 2018