SAS 2025 - SPLASH 2025

SAS 2025 - SPLASH 2025
SPLASH 2025
Sun 12 - Sat 18 October 2025
Singapore
co-located with
ICFP/SPLASH 2025
Attending
Venue (Sunday Workshops): NUS School of Computing
Venue (FARM Performance): Yong Siew Toh Conservatory
Venue (Main Conference): Marina Bay Sands Convention Centre
Hotels: Concorde Hotel Singapore
Hotels: Wyndham Singapore Hotel
Hotels: Rendezvous Hotel Singapore
ICFP/SPLASH 2025
Code of Conduct
Call for Sponsorship
Registration
Travel Information
Explore Singapore
Outdoor Activities
Information for Presenters at National University of Singapore
Information for Presenters at Marina Bay Sands
Information for Session Chairs
Information for Attendees
ICFP/SPLASH Live Streams
Program
ICFP/SPLASH Program
Your Program
Filter by Day
Sun 12 Oct
Mon 13 Oct
Tue 14 Oct
Wed 15 Oct
Thu 16 Oct
Fri 17 Oct
Sat 18 Oct
Tracks
SPLASH 2025
Doctoral Symposium
FARM
OOPSLA
OOPSLA Artifacts
Onward! Essays
Onward! Papers
Posters
SPLASH Keynotes
SPLASH-E
Student Research Competition
ICFP/SPLASH 2025
Tutorials
Volunteers
Workshops
Co-hosted Conferences
ICFP
ICFP
ICFP
Artifacts
ICFP
Keynotes
ICFP
Papers
ICFP
Student Research Competition
ICFP
JFP First Papers
ICFP
Diversity, Equity, and Inclusion
MPLR
Workshops
Erlang
FARM
FUNARCH
HATRA
HOPE
IWACO
LMPL
miniKanren
ML Family Workshop
OCaml
OlivierFest
PAINT
PLMW @ ICFP/SPLASH
PROPL
REBASE
Scheme
Sponsor Invited Talks
The Scala Workshop
The Scala Workshop
- Where Are We With Scala's Capabilities?
- Simpler Scala Builds with Functional and Object-Oriented Programming
TyDe
VMIL
WebAssembly Workshop
@ ICFP/SPLASH
Co-hosted Symposia
Haskell
SAS
SAS
SAS
Artifact
Organization
SPLASH 2025 Committees
Organizing Committee
Steering Committee
Track Committees
Doctoral Symposium
FARM
Organizing Committee
Program Committee
OOPSLA
OOPSLA Review Committee
External Review / Artifact Evaluation Committee
OOPSLA Artifacts
Onward! Essays
Program Committee
Onward! Steering Committee
Onward! Papers
Program Committee
Steering Committee
Posters
SPLASH-E
Program Commitee
Steering Committee
Student Research Competition
Competition Judges
Review Committee
ICFP/SPLASH
Volunteers
Workshops
Contributors
People Index
Co-hosted Conferences
ICFP
Organizing Committee
Steering Committee
Distinguished Papers Committee
ICFP Artifacts
ICFP Papers
ICFP Student Research Competition
MPLR
Program Committee
Steering Committee
Workshops
Erlang
Organizing Committee
Program Committee
FARM
Organizing Committee
FUNARCH
Program Committee
HATRA
Organizing Committee
Program Committee
HOPE
Program Committee
IWACO
Organizing Committee
LMPL
Organizing Committee
Keynote Speaker
Program Committee
miniKanren
Organizing Committee
Program Committee
ML Family Workshop
Program Committee
OCaml
Program Committee
OlivierFest
Program Committee
PAINT
Organizing Committee
Program Committee
PLMW @ ICFP/SPLASH
Program Committee
PROPL
Program Committee
Organising Committee
REBASE
Organizing Committee
Scheme
Organizing Committee
Program Committee
Sponsor Invited Talks
Organizing Committee
The Scala Workshop
Organizing Committee
Program Committee
TyDe
Organising Committee
Program Committee
VMIL
Organizing Committee
Program Committee
WebAssembly Workshop
Organizers
Program Committee
Co-hosted Symposia
Haskell
Program Committee
SAS
SAS 2025
Program Committee
SAS 2025
Steering Committee
SAS Artifact
Series
Series
SPLASH 2026
SPLASH 2025
SPLASH 2024
SPLASH 2023
SPLASH 2022
SPLASH 2021
SPLASH 2020
SPLASH 2019
SPLASH 2018
SPLASH 2017
SPLASH 2016
SPLASH 2015
SPLASH 2014
SPLASH 2013
SPLASH 2012
SPLASH 2011
SPLASH 2010
OOPSLA 2009
OOPSLA 2008
OOPSLA 2007
OOPSLA 2006
OOPSLA 2005
OOPSLA 2004
OOPSLA 2003
OOPSLA 2002
OOPSLA 2001
OOPSLA 2000
ICFP/SPLASH 2025
series
) /
SPLASH 2025
series
) /
SAS 2025 (
series
) /
SAS 2025
About
Program
Accepted Papers
Call for Papers
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, October 13–14, 2025, Proceedings
Cousot Young Researcher Best Paper Award
Title
Relating Distances and Abstractions: An Abstract Interpretation Perspective
SAS
Marco Campion
Isabella Mastroeni
Caterina Urban
Dates
Plenary
Program Display Configuration
Close
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
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
10:10
40m
Coffee break
Break
ICFP/SPLASH Catering
10:50 - 12:05
Opening and Keynote
SAS
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
National University of Singapore
File Attached
12:10 - 13:40
Lunch
ICFP/SPLASH Catering
at
Orchid Dining Hall
12:10
90m
Lunch
Lunch
ICFP/SPLASH Catering
13:40 - 15:20
Verification
SAS
at
Orchid East
Chair(s):
Olivier Danvy
National University of 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
Tom Yuviler
Technion
Dana Drachsler Cohen
Technion
15:20 - 16:00
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
15:20
40m
Coffee break
Break
ICFP/SPLASH Catering
16:00 - 17:40
Abstraction and Proofs
SAS
at
Orchid East
Chair(s):
Xavier Rival
Inria - CNRS - Ecole Normale Superieure de Paris - PSL University
16:00
20m
Talk
Relating Distances and Abstractions: An Abstract Interpretation Perspective
SAS
Marco Campion
Sorbonne Université
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
Alexandre Drewery
INRIA
Thomas P. Jensen
INRIA Rennes
David Pichardie
Meta
17:20
20m
Talk
Abstracting Concolic Execution for Soft Contract Verification
SAS
Bram Vandenbogaerde
Software Languages Lab, Vrije Universiteit Brussel
Quentin Stiévenart
Université du Québec à Montréal
Coen De Roover
Vrije Universiteit Brussel
Pre-print
18:00 - 20:00
ICFP Reception
ICFP Student Research Competition
ICFP/SPLASH Catering
at
Garden Walk
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
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
10:10
40m
Coffee break
Break
ICFP/SPLASH Catering
10:50 - 12:05
Compiler
SAS
at
Orchid East
Chair(s):
Hakjoo Oh
Korea University
10:50
55m
Keynote
From Within: Compiler Testing and Validation via Compilers
SAS
Qirun Zhang
Georgia Institute of Technology
11:45
20m
Talk
Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis
SAS
Adi Harif
Shachar Itzhaky
Technion
12:10 - 13:40
Lunch
ICFP/SPLASH Catering
at
Orchid Dining Hall
12:10
90m
Lunch
Lunch
ICFP/SPLASH Catering
13:40 - 15:20
Abstract Interpretation
SAS
at
Orchid East
Chair(s):
Marco Campion
Sorbonne Université
13:40
60m
Keynote
Towards static analyses and abstract domains for hyperproperties
SAS
Xavier Rival
Inria - CNRS - Ecole Normale Superieure de Paris - PSL University
14:40
20m
Talk
Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
SAS
Matan Shachnai
Harishankar Vishwanathan
Srinivas Narayana
Rutgers University
Santosh Nagarakatte
Rutgers University
Link to publication
Pre-print
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
Coffee break
ICFP/SPLASH Catering
at
Orchid Dining Hall
15:20
40m
Coffee break
Break
ICFP/SPLASH Catering
16:00 - 17:40
Testing and Constraint Solving
SAS
at
Orchid East
Chair(s):
Yahui Song
Standard Chartered Bank
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
Software Languages Lab, Vrije Universiteit Brussel
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
Software Languages Lab, Vrije Universiteit Brussel
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
University of Cambridge
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
Bram Vandenbogaerde
Quentin Stiévenart
Coen De Roover
Pre-print
A Programming Language for Feasible Solutions
SAS
Weijun Chen
Yuxi Fu
Huan Long
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
SAS
Hiroyuki Katsura
Naoki Kobayashi
Ken Sakayori
Ryosuke Sato
Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
SAS
Junda Zheng
Peisen Yao
Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
SAS
Matan Shachnai
Harishankar Vishwanathan
Srinivas Narayana
Santosh Nagarakatte
Link to publication
Pre-print
Contextual Equality Saturation
SAS
Alexandre Drewery
Thomas P. Jensen
David Pichardie
Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters
SAS
Noah Van Es
Bram Vandenbogaerde
Coen De Roover
Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis
SAS
Adi Harif
Shachar Itzhaky
Enhancing Neural Network Robustness via Synthesis of Repair Programs
SAS
Tom Yuviler
Dana Drachsler Cohen
Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
SAS
Jaeseo Lee
Kyungmin Bae
Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
SAS
Bram Vandenbogaerde
Sarah Verbelen
Noah Van Es
Coen De Roover
Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
SAS
Zixin Huang
Jacob Laurel
Saikat Dutta
Sasa Misailovic
Relating Distances and Abstractions: An Abstract Interpretation Perspective
SAS
Marco Campion
Isabella Mastroeni
Caterina Urban
Specifying and Verifying Future Conditions
SAS
Yahui Song
Darius Foo
Wei-Ngan Chin
Verifying Neural Networks with PyRAT
SAS
Tristan Le Gall
Augustin Lemesle
Julien Lehmann
Zakaria Chihani
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.
Important Dates
AoE (UTC-12h)
Mon 13 - Tue 14 Oct 2025
Conference Date
Thu 31 Jul 2025
Camera-Ready
Thu 10 Jul 2025
Notification
Mon 16 Jun - Wed 18 Jun 2025
Author Response
Sun 18 May 2025
Artifact Submission
Sun 11 May 2025
Paper Submission
Submission Link
Program Committee
Hakjoo Oh
Co-chair
Korea University
South Korea
Yulei Sui
Co-chair
University of New South Wales
Australia
Karim Ali
NYU Abu Dhabi
United Arab Emirates
Kyungmin Bae
POSTECH
South Korea
Sébastien Bardin
CEA LIST, University Paris-Saclay
France
Roberto Bruni
University of Pisa
Italy
Liqian Chen
NUDT
China
Lucas C.
Cordeiro
University of Manchester, UK
United Kingdom
Mila
Dalla Preda
University of Verona
Italy
Pierre Ganty
IMDEA Software Institute, Spain
Samir Genaim
Universidad Complutense de Madrid
Spain
Ningyu He
Hong Kong Polytechnic University
Hong Kong SAR China
Quang Loc
Le
University College London
United Kingdom
Pedro López-García
IMDEA Software Institute
Antoine Miné
Sorbonne Université
France
Ashish Mishra
IIT Hyderabad
India
Sidi
Mohamed Beillahi
University of Toronto
Canada
Raphaël Monat
Inria and University of Lille
France
Jorge A.
Navas
Certora
United States
Jihyeok Park
Korea University
South Korea
Goran Piskachev
Amazon Web Services
Germany
Xiaokang Qiu
Purdue University
United States
Xavier Rival
Inria - CNRS - Ecole Normale Superieure de Paris - PSL University
France
Xujie Si
University of Toronto
Gagandeep Singh
University of Illinois at Urbana-Champaign; VMware Research
United States
Sunbeom So
GIST (Gwangju Institute of Science and Technology)
Fu Song
Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software Technology
China
Tian Tan
Nanjing University
China
Mohit Tekriwal
Lawrence Livermore National Laboratory
United States
Manas Thakur
IIT Bombay
India
Caterina Urban
Inria & ENS | PSL
France
Yuepeng Wang
Simon Fraser University
Canada
Peisen Yao
Zhejiang University
China
Jooyong Yi
UNIST
South Korea
Enea Zaffanella
University of Parma
Italy
Qirun Zhang
Georgia Institute of Technology
United States
Xin Zhang
Peking University
China
Steering Committee
Bor-Yuh Evan
Chang
University of Colorado Boulder & Amazon
United States
Patrick Cousot
Cezara Drăgoi
AWS / ENS
Roberto Giacobazzi
University of Arizona
United States
Alessandra Gorla
IMDEA Software Institute
Spain
Manuel Hermenegildo
Technical University of Madrid (UPM) and IMDEA Software Institute
Spain
José Morales
IMDEA Software Institute
Spain
Kedar Namjoshi
Nokia Bell Labs
United States
David Pichardie
Meta
France
Mihaela Sighireanu
University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF
France
Gagandeep Singh
University of Illinois at Urbana-Champaign; VMware Research
United States
Caterina Urban
Inria & ENS | PSL
France
Fri 24 Apr 14:41