ISSTA/ECOOP 2024 (series) / ECOOP 2024 (series) / Technical Papers /
A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson
Verification of smart contracts is an important topic in the context of blockchain technology. We study an approach to verification that is based on symbolic execution.
As a formal basis for symbolic execution, we design a dynamic logic for Michelson, the smart contract language of the Tezos blockchain, and prove its soundness in the proof assistant Agda. Towards the soundness proof we formalize the concrete semantics as well as its symbolic counterpart in a unified setting. The logic encompasses single contract runs as well as inter-contract runs chained in a single transaction.
Wed 18 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Wed 18 Sep
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | VerificationTechnical Papers at EI 2 Pichelmayer Chair(s): João Costa Seco NOVA-LINCS; Nova University of Lisbon | ||
13:30 15mTalk | A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson Technical Papers Barnabas Arvay University of Freiburg, Thi Thu Ha Doan University of Freiburg, Peter Thiemann University of Freiburg, Germany | ||
13:45 15mTalk | Qafny: A Quantum-Program Verifier Technical Papers Liyi Li Iowa State University, Mingwei Zhu University of Maryland, College Park, Rance Cleaveland University of Maryland, Alexander Nicolellis Iowa State University, Yi Lee University of Maryland, College Park, Le Chang University of Maryland, College Park, Xiaodi Wu University of Maryland | ||
14:00 15mTalk | Verifying Lock-free Search Structure Templates Technical Papers Nisarg Patel New York University, Dennis Shasha New York University, Thomas Wies New York University | ||
14:15 15mTalk | Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning Technical Papers | ||
14:30 15mTalk | Compositional Symbolic Execution for Correctness and Incorrectness Reasoning Technical Papers Andreas Lööw Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Caroline Cronjäger Ruhr-Universität Bochum, Petar Maksimović Imperial College London, UK, Philippa Gardner Imperial College London | ||
14:45 15mTalk | Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations Technical Papers Jie Qiu Duolingo, Colin Cai University of California, Berkeley, Sahil Bhatia University of California, Berkeley, Niranjan Hasabnis Code Metal, Sanjit Seshia UC Berkeley, Alvin Cheung University of California at Berkeley | ||
Information for Participants
Wed 18 Sep 2024 13:30 - 15:00 at EI 2 Pichelmayer - Verification Chair(s): João Costa Seco
Info for room EI 2 Pichelmayer: