Formal Reasoning about Financial Systems Workshop

September 1st. Gates 403, Stanford Computer Science

Following SBC’22

Formal methods is a mature field in computer science with excellent tools, including static program analyzers, fuzzers, formal verification tools, Satisfiability Modulo Theories checkers, and more.

Recently, these techniques have been integrated into the industry by companies including Amazon, Certora, Consensys, Facebook, Imandra, Runtime Verification, and Trails of Bits.

This one-day workshop brings together researchers developing tools for reasoning about financial systems and smart contracts. We are particularly interested in DeFi, an emerging suite of applications for decentralized asset management over blockchain technology. DeFi is becoming a major economic vehicle in modern society. The Ethereum blockchain alone already manages more than 235 billion USD worth of assets. One of the basic principles behind DeFi is that the code is law, and computer programs called smart contracts that run on the blockchain dictate the conditions and the effects of asset transactions. This groundbreaking idea has many desirable benefits that originate from trust-minimizing and immutable aspects of decentralized public blockchains. 

However, vulnerabilities in smart contracts and in their applications may be exploited to steal or deny access to assets managed by them. Mitigation and prevention of such damages are challenging and require new software development and security design methodologies. Hundreds of millions in USD value have already been lost due to vulnerabilities in smart contracts. Therefore, smart contract security is a significant concern for DeFi applications. 


08:30-08:55 Neville Grech, & Yannis Smaragdakis, Symvalic Analysis: Overcoming State Explosion in Smart Contracts (remote talk)

08:55-9:20  Leo Alt, Formally Verifying Ethereum Smart Contracts by Overwhelming Horn Solvers (remote talk)

09:20-9:45 Xiaodong LinSODA: A Generic Online Detection Framework for Smart Contracts

09:45-10:00 Break

10:00-10:25 David Dill, The Current State of Move Prover

10:25-10:50 John Toman, Pointer Analysis of Bytecode Programs for Effective Formal Verification of Smart Contracts

10:50-11:15 Grigore Rosu, From fast execution to formal verification of smart contracts using the K Framework

12:00-1:00 Lunch

1:00-1:25  Dimitar Bounov, Property Specification and Instrumentation with Scribble

1:25-1:50 Arie Gurfinkel, Compositional Verification of Smart Contracts Through Communication Abstraction

1:50-14:15  Gustavo Grieco, Digging Deeper into Smart Contracts with Echidna

14:15-14:30 Coffee Break

14:30-14:55 Yoni Zohar, Int-Blasting

14:55-15:20 Jakob Rath, Polysat: Precise Large Word-Level Arithmetic Reasoning about Low-Level Code Snippets

14:20-15:55  Sam Blackshear, Move: A Cross-Platform Language for Safe Programming with Assets

15:55-16:10 Break

16:10-16:35   Marco Eilers, Rich Specifications for Ethereum Smart Contract Verification

16:35-17:00  George Pîrlea, Practical Smart Contract Shardingwith Ownership and Commutativity Analysis

17:00-17:25 Yu FengHardening Solidity Smart Contracts with Refinement Types, For Free

17:25 Closing


Clark Barrett, Stanford

Orna Grumberg, Technion

Mooly Sagiv, Certora and Tel Aviv University

Register here

Thank you to our sponsor