SOAP 2025
as the organisers put it
Static and dynamic analysis techniques and tools for mainstream programming languages (such as Java, C, JavaScript), have received widespread attention for a long time. The application domains of these analyses range from core libraries to modern technologies such as web services and mobile applications. Over time, various analysis frameworks have been developed to provide techniques for optimizing programs, ensuring code quality, and assessing security and compliance. SOAP 2025 aims to bring together the members of the program analysis community to share new developments and shape innovat ...
who it's for
program analysis researchers, static analysis engineers, tool builders for large codebases, security engineers, compiler and tooling engineers, mobile app developers
topics
polynomial loop synthesis with algebraic geometry; data flow graph extraction for C-to-Rust; bit-level dominance preserving quantization; whole-program program dependence graphs; compositional static callgraph reachability; matrix-multiplication CFL-reachability; scaling IFDS data-flow analyses; language-agnostic taint tracking via data dependencies; sequence abstraction for shape and value analysis; practical trade-offs in call-graph precision
| title | author | length |
|---|---|---|
| Beyond Affine Loops: A Geometric Approach to Program Synthesis | Erdenebayar Bayarmagnai, Fatemeh Mohammadi, Rémi Prébet | 19m |
Claims it reduces loop synthesis to solving finite polynomial systems by computing a finite set of polynomial equations whose solutions enumerate all… | ||
| Optimizing Type Migration for LLM-Based C-to-Rust Translation: A Data Flow Graph Approach | Qingxiao Xu, Jeff Huang | 15m |
Manual translation of the Gzip C package using LLMs and static analysis documents concrete fixes: extract data flow graphs with CLAN, prompt o1/ChatGPT01 to… | ||
| Towards Bit-Level Dominance Preserving Quantization of Neural Classifiers | Dorra Ben Khalifa, Matthieu Martel | 23m |
Method computes the minimum bit precision PR that guarantees the original predicted class remains unchanged for all inputs, giving a static, per-layer… | ||
| Building X-Ray for enterprise-scale software | Charles Zhang | 01h 00m |
Clearblue lifts production binaries into LMIR and builds a whole‑program PDG stored on disk to answer value‑flow queries; it analyzes the Linux kernel… | ||
| Compositional Static Callgraph Reachability Analysis for WhatsApp Android App Health | Akos Hajdu, Roman Lee, Gavin Weng, Nilesh Agrawal, Jérémy Dubreil | 29m |
Compositional static callgraph reachability, implemented as an Infer static analyzer checker with Java annotations and regex specs plus source/sync… | ||
| Universal High-Performance CFL-Reachability via Matrix Multiplication | Ilia Muravev, Semyon Grigorev | 21m |
FastMatrixCFPQ implements a universal, matrix-based CFL-reachability solver built on SuiteSparse:GraphBLAS that uses delta-matrix multiplication, boolean… | ||
| Pick Your Call Graphs Well: On Scaling IFDS-Based Data-Flow Analyses | Kadiray Karakaya, Palaniappan Muthuraman, Eric Bodden | 19m |
The paper builds QCG extends Qilin and integrates with FlowDroid to measure how call-graph precision affects IFDS taint analyses on TaintBench (39 apps)… | ||
| Scalable Language Agnostic Taint Tracking using Explicit Data Dependencies | Sedick David Baker, Xavier Pinho, Andrei Michael Dreyer, Fabian Yamaguchi | 19m |
Implements a language-agnostic, whole-program data-dependence graph on top of Joern/CPG that initially over-approximates all call-site flows so libraries can… | ||
| The MemCAD static analyser: shape, value and collection abstraction and application to(…) | Xavier Rival | 01h 02m |
MemCAD implements a new sequence abstraction for unbounded sequences and plugs it into a reduced product of shape and value domains so the analyzer tracks… | ||
| nothing matches | ||