SAS 2025
as the organisers put it
Welcome to the website of the 32nd Static Analysis Symposium (SAS 2025). 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 for more than 30 years as the primary venue for the presentation of theoretical, practical, and application advances in the area. The Symposium will be held from October 13-14 at the Marina Bay Sands Convention Centre. Static Analysis 32nd International Symposium, SAS 2025, Singapore, Singapore, Oct ...
who it's for
static analysis researchers, formal verification engineers, compiler developers, SMT solver developers, security and robustness engineers, embedded and control systems engineers
topics
contextual equality saturation; contextual e-graphs; SMT solver differential testing; delta store semantics; abstract garbage collection; catamorphism synthesis for CHCs; Lean symbolic model checking; future-condition Hoare rules; abstract domains for hyperproperties; neural network repair synthesis; executable PLC networked semantics; precision testing of eBPF operators
| title | author | length |
|---|---|---|
| Contextual Equality Saturation | Alexandre Drewery, Thomas P. Jensen, David Pichardie | 17m |
Extends equality saturation so rewriting can occur under local branch assumptions, replacing costly swap laws with contextual rewriting rules that match a… | ||
| Bounded-Exhaustive Subspace Diversification for SMT Solver Testing | Junda Zheng, Peisen Yao | 21m |
Canary runs differential testing on Z3 and CVC5 and systematically partitions solutions with three bounded mutation strategies — numerical domains, boolean… | ||
| Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters | Noah Van Es, Bram Vandenbogaerde, Coen De Roover | 22m |
A semantics change returns a delta store (partial map of only changed addresses) instead of an updated store, enabling a single evaluation rule to interleave… | ||
| Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…) | Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato | 18m |
A procedure automatically abstracts CHCs over algebraic data types to integer CHCs by synthesizing catamorphisms (generalized folds) via a CEGAR-style loop… | ||
| Multi-Modal Verification of Distributed Systems in Lean | Ilya Sergey | 01h 01m |
Framework called Veil (Lean library) encodes transition systems as shallow Lean programs, generates verification conditions sent to SMT solvers and falls back… | ||
| Specifying and Verifying Future Conditions | Yahui Song, Darius Foo, Wei-Ngan Chin | 23m |
Proposes over-approximating Hoare-style forward rules that embed future-condition obligations into program states so each event is processed once, plus a bag… | ||
| Relating Distances and Abstractions: An Abstract Interpretation Perspective | Marco Campion, Isabella Mastroeni, Caterina Urban | 21m |
Formalizes when a pre-metric induces an upper closure operator (uco) via Galois connections, showing uco-representable prematrices form a strict subset and… | ||
| Towards static analyses and abstract domains for hyperproperties | Xavier Rival | 59m |
Outlines concrete static-analysis routes for hyperproperties: noninterference is two-safety / K-safety with counterexamples of K executions, reduced to safety… | ||
| Enhancing Neural Network Robustness via Synthesis of Repair Programs | Tom Yuviler, Dana Drachsler Cohen | 23m |
A stochastic enumerative synthesizer named DefEnSyn generates short repair programs that change a few latent features via simple arithmetic assignments, learns… | ||
| On a simple problem due to Yves Bertot | Olivier Danvy | 43m |
Starts from Bertot’s puzzle that the product of two consecutive naturals is even and proves the general claim that the product of m consecutive integers is… | ||
| Formal Analysis of Networked PLC Controllers Interacting with Physical Environments | Jaeseo Lee, Kyungmin Bae | 20m |
A unified, executable semantics combines K-based semantics for PLC programs, rewrite-based real-time ticks for continuous dynamics and an object model for… | ||
| Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential(…) | Matan Shachnai, Harishankar Vishwanathan, Srinivas Narayana, Santosh Nagarakatte | 19m |
Presents a reproducible pipeline that lifts the 30,000-line eBPF verifier C code (about 6,000 lines of abstract-operator logic) into SMT via LLVM, checks… | ||
| Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and(…) | Adi Harif, Shachar Itzhaky | 25m |
Ductape ahead-of-time compiles TypeScript by building a program-dependence IR, running a Datalog-based pointer analysis and sound fixpoint type inference that… | ||
| Verifying Neural Networks with PyRAT | Tristan Le Gall, Augustin Lemesle, Julien Lehmann, Zakaria Chihani | 20m |
PyRAT is a Python verifier that uses abstract interpretation with intervals, zonotopes and constrained zonotopes, is sound for floating‑point ops, and ingests… | ||
| From Within: Compiler Testing and Validation via Compilers | Qirun Zhang | 53m |
Claims a compiler-centric workflow that instruments LLVM APIs to record instruction manipulations and debug-location updates, then compares those traces to a… | ||
| nothing matches | ||