SAS 2021
as the organisers put it
Welcome to the 28th Static Analysis Symposium (SAS 2021)! 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. SAS begins this Sunday! We are looking forward to inspirational talks and enjoyable discussions! Please join us. The SAS proceedings is now available, with free access for 4 months. We are very happy to anno ...
who it's for
static analysis researchers, formal verification engineers, programming language researchers, tool developers, compiler engineers, software security analysts, systems researchers
topics
Solidity contract abstraction; hash-consed points-to sets; Python-C interlanguage analysis; symbolic automatic relations to CHC; reduced-product domains for neural nets; input quantization for ACAS Xu verification; Datalog library-value merging (4DM); floating-point attacks on network verification; tropical polyhedra for ReLU nets; release-acquire thread-modular analysis; endian portability by abstract interpretation; selectively-amortized resource analysis
| title | author | length |
|---|---|---|
| Compositional Verification of Smart Contracts Through Communication Abstraction | Scott Wesley, Maria Christakis, Arie Gurfinkel, Jorge A. Navas, Richard Trefler, Valentin Wüstholz | 15m |
Claims a local bundle abstraction that reduces Solidity contracts with 2^160 addresses to a few representative users (example: 2^160 → 4) and turns… | ||
| Hash Consed Points-To Sets | Mohamad Barbar, Yulei Sui | 13m |
Implements hash-consed, interned points-to sets and operation tables inside the LLVM/SVF framework, changing only the data structure not the algorithm… | ||
| A Multi-Language Static Analysis of Python Programs with Native C Extensions | Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné | 14m |
An abstract interpreter called Mopsa automatically analyzes both Python and native C sources, modeling language switches and reporting runtime errors in… | ||
| Symbolic Automatic Relations and Their Applications to SMT and CHC Solving | Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato | 15m |
Defines symbolic automatic relations that combine symbolic automata and automatic relations and proves they are closed under Boolean ops; shows satisfiability… | ||
| Reduced Products of Abstract Domains for Fairness Certification of Neural Networks | Denis Mazzucato, Caterina Urban | 15m |
Tool analyzes ReLU feed‑forward classifiers and first runs a forward pre-analysis that splits the input space by counting uncertain ReLUs against configurable… | ||
| Verifying Low-dimensional Input Neural Networks via Input Quantization | Kai Jia, Martin C. Rinard | 08m |
Prepending an input quantization layer maps every low‑dimensional input to the original ACAS Xu grid so pretrained networks need no retraining and run… | ||
| Accelerating Program Analyses in Datalog by Merging Library Facts | Yifan Chen, Chenyang Yang, Xin Zhang, Yingfei Xiong, Hao Tang, Xiaoyin Wang, Lu Zhang | 13m |
Proposes 4DM, a Datalog transformation that inserts Abstract relations to merge sensitivity-domain values (e.g., contexts) so analyses run fewer times while… | ||
| Exploiting Verified Neural Networks via Floating Point Numerical Error | Kai Jia, Martin C. Rinard | 11m |
A verification gap lets machine-precision disagree with the verifier: using MIPVerify on CIFAR10 and MNIST with a 2/255 bound the authors programmatically… | ||
| Static analysis of ReLU neural networks with tropical polyhedra | Eric Goubault, Sebastien Palumby, Sylvie Putot, Louis Rustenholz, Sriram Sankaranarayanan | 14m |
This work abstracts ReLU feedforward nets with tropical polyhedra and a zone abstraction to compute tight output ranges, proving concrete claims: it verifies… | ||
| Selectively-Amortized Resource Bounding | Tianhan Lu, Bor-Yuh Evan Chang, Ashutosh Trivedi | 14m |
Presents a framework that proves resource bounds by mixing worst-case and amortized reasoning, proves any partitioning into amortization segments sound, and… | ||
| Thread-modular Analysis of Release-Acquire Concurrency | Divyanjali Sharma, Subodh Sharma | 15m |
A thread-modular abstract-interpretation method targets RA (release-acquire) programs by encoding per-variable modification orders as a PO domain and using an… | ||
| Improving Thread-Modular Abstract Interpretation | Michael Schwarz, Simon Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani | 15m |
Formalizes thread-modular non-relational value analyses with a new local trace semantics and a side-effecting constraint-system framework, casts Goblint’s… | ||
| Static Analysis of Endian Portability by Abstract Interpretation | David Delmas, Abdelraouf Ouadjaout, Antoine Miné | 14m |
A static analysis based on abstract interpretation proves when two endian-specific C variants produce identical outputs on identical inputs, despite pointer… | ||
| Selective Context-Sensitivity for k-CFA with CFL-Reachability | Jingbo Lu, Dongjie He, Jingling Xue | 13m |
Presents a concrete method that uses CFL-reachability pre-analysis to decide which program nodes need k-CFA context-sensitivity, builds a fast verifier that… | ||
| Verified Functional Programming of an Abstract Interpreter | Lucas Franceschino, David Pichardie, Jean-Pierre Talpin | 13m |
Claims a fully implemented abstract interpreter in the F verified programming environment that proves soundness while keeping proofs tiny: about 40 lines of… | ||
| Automated Verification of the Parallel Bellman--Ford Algorithm | Mohsen Safari, Wytse Oortwijn, Marieke Huisman | 15m |
First deductive verification of an unoptimized GPU Bellman–Ford: mechanized proof shows data-race freedom plus soundness and completeness of shortest distances… | ||
| Fast and Efficient Bit-Level Precision Tuning | Assalé Adjé, Dorra Ben Khalifa, Matthieu Martel | 14m |
POP implements a semantics-driven precision tuner that generates an ILP from source code (solved with GLPK) to pick optimal bit widths, and a refined solver… | ||
| Data Abstraction: A General Framework to Handle Program Verification of Data Structures | Julien Braine, Laure Gonnord, David Monniaux | 13m |
Proposes a constructive reduction that turns universally quantified array properties like “all elements below index i are nonzero” into a purely scalar… | ||
| Automatic Synthesis of Data-Flow Analyzers | Xuezheng Xu, Xudong Wang, Jingling Xue | 15m |
A tool called DFASy automatically synthesizes intraprocedural, path‑insensitive data‑flow analyzers from a CFG plus expected before/after facts, producing flow… | ||
| Disjunctive Interval Analysis | Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sondergaard, Peter J. Stuckey | 15m |
Proposes range decision diagrams (RDDs) as a compact Boxes implementation that avoids constraint substitution and no dependence on a theory solver, and that… | ||
| Toward Neural-Network-Guided Program Synthesis and Verification | Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno | 15m |
Proposes NeuGuS, a gray-box method that trains neural nets (four-layer; sometimes three-layer) then extracts inequalities from weights/biases to build Boolean… | ||
| Backward Symbolic Execution with Loop Folding | Marek Chalupa, Jan Strejcek | 13m |
Presents backward symbolic execution with loop folding that proves error unreachability by deriving inductive, often disjunctive loop invariants from backward… | ||
| nothing matches | ||