Wed 23 Oct 2024 19:31 - 19:40 at California - Posters

Blockchain technologies are applied in diverse domains such as financial systems, supply chains, and identity management, leading to the emergence of various smart contract languages design. These contracts often involve time dependent transactions recorded immutably on the blockchain, making their correctness crucial. This paper addresses the formal verification of temporal behaviors in smart contracts without human interaction. We study 9 recent smart contract languages used in 7 leading blockchains and model 27 common temporal patterns from 3148 benchmarks across 9 domain specific application categories. We introduce VESC, a temporal specification language that allows developers to specify temporal properties in structured natural language, which VESC compiles into formal linear temporal logic. Our experiments demonstrate that VESC effectively specifies common temporal behaviors, paving the way for automated temporal verification of smart contracts.

Wed 23 Oct

Displayed time zone: Pacific Time (US & Canada) change

17:40 - 19:40
17:40
8m
Poster
AUTOINC: Incrementality for Free
Posters
17:48
8m
Poster
Meerkat: Distributed Reactive Live Semantics with Causal Consistency
Posters
17:57
8m
Poster
Ordering Rejectable Stacks in SGLR Parsing
Posters
Jeff Smits Delft University of Technology, Daniel A. A. Pelsmaeker Delft University of Technology, Netherlands
18:05
8m
Poster
TickTalk: A Programming Language and System for Distributed, Time-Sensitive Applications
Posters
Kyle Liang Carnegie Mellon University, Edward Andert Arizona State University, Aviral Shrivastava Arizona State University, Jonathan Aldrich Carnegie Mellon University
18:14
8m
Poster
Algebraic effect handlers with bidirectional type-checking
Student Research Competition
18:22
8m
Poster
A Parameterized Framework for the Formal Verification of Zero-Knowledge Virtual Machines
Student Research Competition
Youwei Zhong Shanghai Jiao Tong University
18:31
8m
Poster
Automatically Generating an Abstract Interpretation-based Optimizer from a DSL
Student Research Competition
18:40
8m
Poster
Automatic Local Inverse Calculation for Change of Variables
Student Research Competition
18:48
8m
Poster
Design of Fractional Permissions for a Gradual Verifier
Student Research Competition
18:57
8m
Poster
Grammar Derivation Visualization in Automata Theory
Student Research Competition
19:05
8m
Poster
Kawa: An Abstract Language for Scalable and Variable Detection of Spectre Vulnerabilities
Student Research Competition
Zheyuan Wu , Haoyi Zeng , Aaron Bies Saarland University
19:14
8m
Poster
Towards a Formal Approach to the Analysis of Human-Machine Interaction
Student Research Competition
Leyi Cui Columbia University, New York
19:22
8m
Poster
Understanding Program Visualizations in the Wild
Student Research Competition
Joel Castro University of California, Berkeley, Olohi Goodness John Smith College
19:31
8m
Poster
VESC:Towards Temporal Verification of Smart Contracts
Student Research Competition
Samuel Larsen , Kevin Johanson , Cyrus Liu Samsung Semiconductor
DOI