This book constitutes the refereed proceedings of the 32nd International Static Analysis Symposium, SAS 2025, held in Singapore, Singapore, in October 2025.

The 15 papers included here were carefully reviewed and selected from 32 submissions.

The papers presented in this book deal with abstract interpretation, automated deduction, data flow analysis, debugging techniques, deductive methods, emerging applications, model checking, data science, program optimizations and transformations, program synthesis, program verification, machine learning and verification, security analysis, tool environments and architectures, theoretical frameworks, type checking, distributed or networked systems, and LLM for static analysis and static analysis for LLM.

Inhalt

.- On a simple problem due to Yves Bertot.

.- Verifying Neural Networks with PyRAT.

.- Contextual Equality Saturation.

.- A Programming Language for Feasible Solutions.

.- Specifying and Verifying Future Conditions.

.- AURA: Precise Abstract Interpretation of Probabilistic Programs with
Interval Data Uncertainty.

.- Comparing the Precision of Abstract Operators in the eBPF Verifier
using Differential Synthesis.

.- Bounded-Exhaustive Subspace Diversification for SMT Solver Testing.

.- Abstracting Concolic Execution for Soft Contract Verification.

.- Enhancing Neural Network Robustness via Synthesis of Repair Programs.

.- Relating Distances and Abstractions: An Abstract Interpretation
Perspective.

.- Ductape: Optimizing Dynamically Typed Programs Using
Ahead-of-Time Compilation and Data-Flow Analysis.

.- Automated Catamorphism Synthesis for Solving Constrained Horn
Clauses over Algebraic Data Types.

.- Formal Analysis of Networked PLC Controllers Interacting with
Physical Environments.

.- Monarch: A Modular Framework for Abstract Definitional Interpreters
in Haskell.

.- Delta Store Semantics: Abstract Garbage Collection for Abstract
Definitional Interpreters.