A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson (ECOOP 2024 - Technical Papers)

Who

Barnabas Arvay, Thi Thu Ha Doan, Peter Thiemann

Track

ECOOP 2024 Technical Papers

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect 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

Wed 18 Sep 2024 13:30 - 13:45 at EI 2 Pichelmayer - Verification

Abstract

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.

Barnabas Arvay

University of Freiburg

Thi Thu Ha Doan

University of Freiburg

Peter Thiemann

University of Freiburg, Germany

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

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

Time Band

Display full programSpecify a time band

Save

Session Program

Wed 18 Sep
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00	VerificationTechnical Papers at EI 2 Pichelmayer

13:30 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning Technical Papers Stephen N. Freund Williams College, Cormac Flanagan University of California at Santa Cruz
14:30 15m Talk		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 15m Talk		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 Intel Labs, 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

Info for room EI 2 Pichelmayer:

Map: https://tuw-maps.tuwien.ac.at/?q=CF0235

Room tech: https://www.tuwien.at/en/tu-wien/organisation/central-divisions/real-estate-and-facility-management/event-services-and-lecture-hall-support/room-database/lecture-halls/ei-2-pichelmayer