SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Mon 18 Oct 2021 11:05 - 11:20 at Zurich B - Session 2B Chair(s): Cezara Drăgoi
Mon 18 Oct 2021 19:05 - 19:20 at Zurich B - Session 2B Chair(s): Suvam Mukherjee

We consider the problem of automatically proving resource bounds. That is, we study how to prove that an integer-valued resource variable is bounded by a given program expression. Automatic resource-bound analysis has recently received significant attention because of a number of important applications (e.g., detecting performance bugs, preventing algorithmic-complexity attacks, identifying side-channel vulnerabilities), where the focus has often been on developing precise amortized reasoning techniques to infer the most exact resource usage. While such innovations remain critical, we observe that fully precise amortization is not always necessary to prove a bound of interest. And in fact, by amortizing selectively, the needed supporting invariants can be simpler, We present a framework for selectively-amortized analysis that mixes worst-case and amortized reasoning via a property decomposition and a program transformation. We show that proving bounds in any such decomposition yields a sound resource bound in the original program, and we give an algorithm for selecting a reasonable decomposition.

Mon 18 Oct

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

10:50 - 12:10
Session 2BSAS at Zurich B +8h
Chair(s): Cezara Drăgoi Inria / ENS / Informal Systems
10:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication AbstractionVirtual
SAS
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Arie Gurfinkel University of Waterloo, Jorge A. Navas SRI International, Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys
Pre-print
11:05
15m
Talk
Selectively-Amortized Resource BoundingVirtual
SAS
Tianhan Lu University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Ashutosh Trivedi
Pre-print
11:20
15m
Talk
Thread-modular Analysis of Release-Acquire ConcurrencyVirtual
SAS
Divyanjali Sharma IIT Delhi, India, Subodh Sharma IIT Delhi
11:35
35m
Live Q&A
Session 2B Discussion, Questions and Answers
SAS

18:50 - 20:10
Session 2BSAS at Zurich B
Chair(s): Suvam Mukherjee Microsoft Research
18:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication AbstractionVirtual
SAS
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Arie Gurfinkel University of Waterloo, Jorge A. Navas SRI International, Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys
Pre-print
19:05
15m
Talk
Selectively-Amortized Resource BoundingVirtual
SAS
Tianhan Lu University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Ashutosh Trivedi
Pre-print
19:20
15m
Talk
Thread-modular Analysis of Release-Acquire ConcurrencyVirtual
SAS
Divyanjali Sharma IIT Delhi, India, Subodh Sharma IIT Delhi
19:35
35m
Live Q&A
Session 2B Discussion, Questions and Answers
SAS