SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

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.

Dates
Plenary

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 13 Oct

Displayed time zone: Perth change

10:10 - 10:50
10:10
40m
Coffee break
Break
ICFP/SPLASH Catering

10:50 - 12:05
Opening and KeynoteSAS at Orchid East
10:50
10m
Day opening
Opening
SAS

11:05
60m
Keynote
On a simple problem due to Yves Bertot
SAS
Olivier Danvy Yale-NUS College and School of Computing, Singapore
12:10 - 13:40
12:10
90m
Lunch
Lunch
ICFP/SPLASH Catering

13:40 - 15:20
VerificationSAS at Orchid East
Chair(s): Olivier Danvy Yale-NUS College and School of Computing, Singapore
13:40
60m
Keynote
Multi-Modal Verification of Distributed Systems in Lean
SAS
Ilya Sergey National University of Singapore
14:40
20m
Talk
Verifying Neural Networks with PyRAT
SAS
Tristan Le Gall CEA LIST, Augustin Lemesle CEA, LIST, France, Julien Lehmann CEA, LIST, France, Zakaria Chihani CEA, LIST, France
15:00
20m
Talk
Enhancing Neural Network Robustness via Synthesis of Repair Programs
SAS
15:20 - 16:00
15:20
40m
Coffee break
Break
ICFP/SPLASH Catering

16:00 - 17:40
Abstraction and ProofsSAS at Orchid East
Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University
16:00
20m
Talk
Relating Distances and Abstractions: An Abstract Interpretation Perspective
SAS
Marco Campion INRIA & ENS Paris | Université PSL, Isabella Mastroeni University of Verona, Caterina Urban Inria & ENS | PSL
16:20
20m
Talk
Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
SAS
Zixin Huang University of Illinois at Urbana-Champaign, USA, Jacob Laurel Georgia Institute of Technology, Saikat Dutta University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign
16:40
20m
Talk
Specifying and Verifying Future Conditions
SAS
Yahui Song Standard Chartered Bank, Darius Foo National University of Singapore, Wei-Ngan Chin National University of Singapore
17:00
20m
Talk
Contextual Equality Saturation
SAS
17:20
20m
Talk
Abstracting Concolic Execution for Soft Contract Verification
SAS
Bram Vandenbogaerde , Quentin Stiévenart Université du Québec à Montréal, Coen De Roover Vrije Universiteit Brussel
Pre-print
18:00 - 20:00
18:00
2h
Social Event
ICFP SRC Poster Session
ICFP Student Research Competition

Tue 14 Oct

Displayed time zone: Perth change

10:10 - 10:50
10:10
40m
Coffee break
Break
ICFP/SPLASH Catering

12:10 - 13:40
12:10
90m
Lunch
Lunch
ICFP/SPLASH Catering

13:40 - 15:20
Abstract InterpretationSAS at Orchid East
Chair(s): Hakjoo Oh Korea University
13:40
60m
Keynote
Towards static analyses and abstract domains for hyperproperties
SAS
Xavier Rival Inria; ENS; CNRS; PSL University
14:40
20m
Talk
Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
SAS
15:00
20m
Talk
A Programming Language for Feasible Solutions
SAS
Weijun Chen Shanghai Jiao Tong University, China, Yuxi Fu Shanghai Jiao Tong University, China, Huan Long Shanghai Jiao Tong University
15:20 - 16:00
15:20
40m
Coffee break
Break
ICFP/SPLASH Catering

16:00 - 17:40
Testing and Constraint SolvingSAS at Orchid East
16:00
20m
Talk
Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
SAS
Junda Zheng , Peisen Yao Zhejiang University
16:20
20m
Talk
Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
SAS
Bram Vandenbogaerde , Sarah Verbelen Vrije Universiteit Brussel, Belgium, Noah Van Es Sofware Languages Lab, Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel
16:40
20m
Talk
Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters
SAS
Noah Van Es Sofware Languages Lab, Vrije Universiteit Brussel, Bram Vandenbogaerde , Coen De Roover Vrije Universiteit Brussel
17:00
20m
Talk
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
SAS
Hiroyuki Katsura , Naoki Kobayashi University of Tokyo, Ken Sakayori University of Tokyo, Ryosuke Sato Tokyo University of Agriculture and Technology
17:20
20m
Talk
Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
SAS
Jaeseo Lee POSTECH, Kyungmin Bae POSTECH

Accepted Papers

Title
Abstracting Concolic Execution for Soft Contract Verification
SAS
Pre-print
A Programming Language for Feasible Solutions
SAS
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
SAS
Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
SAS
Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
SAS
Contextual Equality Saturation
SAS
Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters
SAS
Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis
SAS
Enhancing Neural Network Robustness via Synthesis of Repair Programs
SAS
Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
SAS
Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
SAS
Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
SAS
Relating Distances and Abstractions: An Abstract Interpretation Perspective
SAS
Specifying and Verifying Future Conditions
SAS
Verifying Neural Networks with PyRAT
SAS

Call for Papers

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 over 30 years as the primary venue for the presentation of theoretical, practical, and application advances in the area.

Topics

The technical program for SAS 2025 will consist of invited lectures and presentations of refereed papers. Contributions are welcomed on all aspects of program analysis analysis, including, but not limited to:

  • 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
  • LLM for static analysis and static analysis for LLM

All paper submissions will be evaluated on the basis of significance, relevance, correctness, originality, and clarity.

We welcome regular papers as well as papers focusing on any of the following in the NEAT (New questions/areas, Experience, Announcement, Tool) category:

  • Well-motivated discussion of new questions or new areas.
  • Experience with static analysis tools, Industrial Reports, and Case Studies
  • Brief announcements of work in progress
  • Tool papers

If you are submitting to the NEAT category rather than as a regular paper, please ensure your submission title is formatted as: “NEAT: your original paper title”. Note that both regular and NEAT submissions share the same page limits.

Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic, object-oriented, aspect, multi-core, distributed, and GPU programming. We do not impose a page limit for submitted papers but we encourage brevity as reviewers have a limited time that they can spend on each paper. With the exception of NEAT papers, all papers will follow a double-blind reviewing process. The identity of the authors for the NEAT papers will be therefore known to the reviewers.

Papers must be written and presented in English. A submitted paper must describe original work and must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal or a conference with refereed proceedings.

All submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. The review process will include a rebuttal period where authors have the opportunity to respond to preliminary reviews on the paper.

Radhia Cousot Award

The program committee will select an accepted regular paper for the Radhia Cousot Young Researcher Best Paper Award in memory of Radhia Cousot and her fundamental contributions to static analysis, as well as being one of the main promoters and organizers of the SAS series of conferences.

Artifacts

As in previous years, we encourage authors to submit a virtual machine image containing any artifacts and evaluations presented in the paper. Artifact submission is optional. Artifact evaluation will be concurrent with paper review. For more details, please visit the SAS 2025 Artifacts page.

Submission Details

Double-Blind Requirement

All regular papers will follow a double-blind process, where author names and affiliations are hidden for the review. To facilitate this process, submitted regular papers must adhere to the following: (1) Author names and affiliations must be omitted and (2) References to the authors’ own related work should be in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”). The purpose of this process is to help the reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission, makes the job of reviewing the paper more difficult, or interferes with the process of disseminating new ideas. For example, important background references should not be omitted or anonymized, even if they are written by the same authors and share common ideas, techniques, or infrastructure.

NEAT Papers Content

New problems papers are an opportunity to discuss visions, challenges, experiences, problems, and impactful solutions in the field of static analysis from both a research and applications perspective. Such papers are encouraged to take assertive positions and be forward-looking and aim for lively and insightful discussions that are influential to future research directions in static analysis. NEAT papers will be handled in singe-blind way. User experience & Industrial reports & Case studies papers describe the use of static analysis in industrial settings or in any chosen application domains. Papers in this category do not necessarily need to present original research results but are expected to contain applications of static analysis as well as a comprehensive evaluation in the chosen application domain. Such papers are encouraged to discuss the unique challenges of transferring research ideas to a real-world setting, reflect on any lessons learned from this technology transfer experience, and compare experiences with different analyzers highlighting their strengths and weaknesses. Brief announcements of work in progress papers may describe work in progress. A submission that is not selected for regular presentation may be invited for a brief announcement.

Submission Guidelines

The SAS 2025 proceedings will be published by Springer in their LNCS series. Authors should consult Springer’s authors’ guidelines and use their proceedings templates, for LaTeX, Overleaf, or Word, for the preparation of their papers. The corresponding author of each accepted paper, acting on behalf of all of the authors of that paper, must complete and sign a Consent-to-Publish form. The corresponding author signing the copyright form should match the corresponding author marked on the paper. Once the files have been sent to Springer, changes relating to the authorship of the papers cannot be made.

Special Issue Invitation

Accepted papers will be invited to submit to a special issue of the Science of Computer Programming (SCP). A SCP publication will require substantial additional material over the conference publication and will undergo a separate review process.