Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contrac...
summary
Asparagus is a tool that takes Solidity/EVM bytecode, over-approximates it into polynomial transition systems, and synthesizes linear or polynomial parametric gas upper-bounds by reducing forall-constraints to existential ones using Farkas’ Lemma, Handelman’s Theorem, Putinar’s Positivstellensatz. It produces SMT-solvable quadratic constraints, runs with a 10s timeout in evaluation, and handles 80.56% of functions (126,269/156,735) across 24,188 contracts, outperforming GASTAP (58.62%) and giving tighter bounds in 97.85% of mutually solved cases.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:43Smart contracts and gas
- 2:06Gas bound challenges
- 3:50Asparagus approach
- 4:31Polynomial transition systems
- 6:38Constraint system solving
- 7:43Farkas' lemma for linear systems
- 10:16Handelman and Putinar theorems
- 12:23Quantifier elimination
- 13:24Experimental results
- 14:08Limitations and failures
- 14:28Conclusion and future
- 14:49Q&A 1
- 15:56Q&A 2
- 16:40Q&A 3
related talks
34mCost Analysis of Smart Contracts via Parametric Resource Analysis
29mSynthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
15mCompositional Verification of Smart Contracts Through Communication Abstraction
29mCompositional Verification of Smart Contracts Through Communication Abstraction
30mConstructing Trustworthy Smart Contracts
21mPractical Verification Of Smart Contracts Using Memory Splitting
21mSolType: Refinement Types for Arithmetic Overflow in Solidity
25mBehavioral simulation for smart contracts