SAS 2020
as the organisers put it
Welcome to the 27th Static Analysis Symposium (SAS 2020)! Static analysis is widely recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The series of Static Analysis Symposia has served as the primary venue for the presentation of theoretical, practical, and application advances in the area.
who it's for
program analysis researchers, tool developers for static analysis, formal methods researchers, programming language researchers, verification engineers, security engineers for smart contracts, compiler developers
topics
parametric gas analysis; polynomial loop invariants; static resource analysis with Infer; abstract neural networks; multi-language abstract semantics; separation logic transformer summaries; predicate abstraction with CEGAR for νHFL; exact gas-cost analysis and amortization; Farkas-based tree interpolation; probabilistic Lipschitz analysis of networks; library modeling language for C programs; memory-efficient fixpoint computation
| title | author | length |
|---|---|---|
| Cost Analysis of Smart Contracts via Parametric Resource Analysis | Manuel Hermenegildo | 34m |
Claims a reusable method that automatically infers safe parametric bounds for gas and storage and delivers concrete formulas by translating contracts to Horn… | ||
| Polynomial Invariants for Affine Programs | James Worrell | 32m |
Claims an algorithm that computes a finite basis of all polynomial invariants for affine loops by reducing invariant synthesis to algebraic-geometry problems… | ||
| Static Resource Analysis at Scale | Ezgi Çiçek | 25m |
Static analysis computes symbolic upper bounds via Infer using an abstract interpretation pipeline that produces summaries and numeric ranges from InferBo… | ||
| Abstract Neural Networks | Matthew Sotoudeh, Aditya V. Thakur | 19m |
Paper claims a procedure to compress a large DNN into a smaller Abstract Neural Network (ANN) that soundly over-approximates every input-output behavior, and… | ||
| On Multi-Language Abstraction: Towards a Static Analysis of Multi-Language Programs | Samuele Buro, Roy Crole, Isabella Mastroeni | 20m |
Paper gives a general, provable method to build an abstract semantics for a language obtained by combining two languages: it lifts concrete algebras to… | ||
| Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries | Hugo Illous, Matthieu Lemerre, Xavier Rival | 20m |
Builds context-sensitive procedure summaries as relational transformations over separation logic (pairs of input/output heap descriptions h# and t#)… | ||
| Predicate Abstraction and CEGAR for nuHFL(Z) Validity Checking | Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada | 19m |
Proposes an algorithm that combines νHFL(ℤ) predicate abstraction with predicate abstraction and CEGAR to decide higher‑order CHC/νHFL(ℤ) validity, implements… | ||
| Exact and Linear-Time Gas-Cost Analysis | Ankush Das, Shaz Qadeer | 18m |
A static tool called GasBoX computes exact gas bounds and removes runtime gas accounting by inserting Gas.deposit and amortizing gas into data with gas… | ||
| Formal framework for reasoning about the precision of dynamic analysis | Mila Dalla Preda, Roberto Giacobazzi, Niccolò Marastoni | 20m |
Provides a formal framework that models dynamic-analysis precision by treating trace properties as equivalence relations and defining obfuscation as… | ||
| Farkas-Based Tree Interpolation | Sepideh Asadi, Martin Blicha, Antti Hyvärinen, Grigory Fedyukovich, Natasha Sharygina | 19m |
Paper studies Farkas-lemma based interpolation for quantifier-free linear real arithmetic (SMT) and classifies five algorithms by whether they guarantee tree… | ||
| Probabilistic Lipschitz Analysis of Neural Networks | Ravi Mangal, Kartik Sarangmath, Aditya V. Nori, Alessandro Orso | 19m |
Defines probabilistic Lipschitzness: for pairs sampled from a generative input model, nearby inputs map to nearby outputs with high probability. Models inputs… | ||
| A Library Modeling Language for the Static Analysis of C Programs | Abdelraouf Ouadjaout, Antoine Miné | 19m |
Language for writing library stubs as logic formulas that model non-deterministic side effects (allocations, assigns with primed output variables) and… | ||
| Simple and Efficient Computation of Minimal Weak Control Closure | Abu Naser Masud | 20m |
Method computes minimal weak control closure by identifying V-paths and locating “weakly deciding vertices” via a backward traversal that builds an… | ||
| Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis | Anastasiia Izycheva, Eva Darulova, Helmut Seidl | 20m |
Method synthesizes floating-point loop invariants by combining counterexample-guided synthesis with random simulation and a noisy polynomial fit for candidate… | ||
| Termination of Polynomial Loops | Florian Frohn, Marcel Hark, Jürgen Giesl | 19m |
Decides termination for a concrete class: triangular weakly non-linear loops admit computable poly-exponential closed forms for variable values, substitution… | ||
| Stratified Guarded First-Order Transition Systems | Christian Müller, Helmut Seidl | 20m |
Defines a class of first-order transition systems that is stratified and strictly guarded, shows weakest-precondition fixpoint iteration eliminates… | ||
| Memory-Efficient Fixpoint Computation | Sung Kook Kim, Arnaud Venet, Aditya V. Thakur | 16m |
A technique interleaves assertion checks with Bourdoncle-style recursive fixpoint iteration to free abstract values early, implemented as MIKOS extends IKOS… | ||
| nothing matches | ||