Welcome to the website of the 33rd Static Analysis Symposium (SAS 2026). 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 6th to 8th at the Oakland Marriott City Centre hotel.

The winner of the 2026 Radhia Cousot Young Researcher Best Paper Award is Sebastien Bonduelle for the paper Determinism Analysis and its Application to Evaluation Order Independence.

Static Analysis 33rd International Symposium, SAS 2026, Oakland, CA, USA, October 6–8, 2026, Proceedings

Keynotes and Tutorials

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

Tue 6 Oct

Displayed time zone: Pacific Time (US & Canada) change

08:30 - 10:00
FoundationsSAS at Grand Ballroom Salons C
Chair(s): David Pichardie Meta
08:30
5m
Day opening
Welcome
SAS
Sébastien Bardin CEA List - Université Paris-Saclay, Aditya V. Thakur University of California at Davis
08:35
30m
Talk
Relaxed Residuation Theory - From Inversion to Abstract Interpretation beyond Classical Adjunctions
SAS
Isabella Mastroeni University of Verona
09:05
30m
Talk
Rocq Bottom: Beyond Soundness with Precise Reasoning about Analysis Precision
SAS
Matthieu Lemerre Université Paris-Saclay - CEA LIST
09:35
30m
Talk
Generator-Dense Galois Connections
SAS
Marco Campion Sorbonne Université, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Antoine Miné Sorbonne Université, Caterina Urban Inria - École Normale Supérieure
10:30 - 12:00
Quantum ComputingSAS at Grand Ballroom Salons C
Chair(s): Sébastien Bardin CEA List - Université Paris-Saclay
10:30
60m
Keynote
Static Analysis of Quantum Programs
SAS
Jens Palsberg University of California at Los Angeles
11:30
30m
Talk
GPU-Accelerated Host-Aware Dead-Measurement Detection in Hybrid Quantum--Classical Programs
SAS
Yanbin Chen Technical University of Munich, Qunyou Liu EPFL, Yu Wang Technical University of Munich, Christian Mendl Technical University of Munich, Helmut Seidl TU Munich
13:30 - 15:00
AbstractionsSAS at Grand Ballroom Salons C
Chair(s): Isabella Mastroeni University of Verona
13:30
30m
Talk
A Lattice of Union-Finds
SAS
Dorian Lesbre Université Paris-Saclay - CEA LIST, Matthieu Lemerre Université Paris-Saclay - CEA LIST
14:00
30m
Talk
A Modular Framework for Stack-Heap and Value Abstractions
SAS
Giacomo Boldini Ca' Foscari University of Venice, Luca Negrini Ca’ Foscari University of Venice, Luca Olivieri University Ca' Foscari, Venice, Pietro Ferrara Ca’ Foscari University of Venice
14:30
30m
Talk
Shape Abstraction of Thread Interferences
SAS
Valentin Barbazo École Normale Supérieure | Université PSL, Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University
15:30 - 17:00
Thread-Modular Abstract InterpretationSAS at Grand Ballroom Salons C
Chair(s): Aditya V. Thakur University of California at Davis
15:30
90m
Tutorial
Thread-Modular Abstract Interpretation with Goblint
SAS
Michael Schwarz National University of Singapore, Vesal Vojdani University of Tartu

Wed 7 Oct

Displayed time zone: Pacific Time (US & Canada) change

08:30 - 10:00
Information Flow and PrivacySAS at Grand Ballroom Salons E+F+G+H
Chair(s): Sébastien Bardin CEA List - Université Paris-Saclay
09:00
30m
Talk
PEG for information flow: analysis and incremental reasoning
SAS
09:30
30m
Talk
Verifying ε-Differential Privacy Bit by Bit
SAS
Zach Susag Grinnell College, Justin Hsu Cornell University
10:30 - 12:00
Agentic ReasoningSAS at Grand Ballroom Salons E+F+G+H
Chair(s): Aditya V. Thakur University of California at Davis
10:30
45m
Keynote
Agentic Code Reasoning
SAS
Satish Chandra Meta Platforms, Inc.
11:15
30m
Talk
NEAT: Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysis
SAS
Jacqueline L. Mitchell University of Southern California, Chao Wang University of Southern California
13:30 - 15:00
Bug Detection, Control Flow & Resource AnalysisSAS at Grand Ballroom Salons E+F+G+H
Chair(s): Hakjoo Oh Korea University
13:30
30m
Talk
FINDUS: Static Detection of Use-After-Scope Violations for Multi-threaded Programs
SAS
Maruti Sairam Venkata Annaluru IIT Hyderabad, Siddhartha Neyagapula IIT Hyderabad, Raj Ambekar IIT Hyderabad, Ramakrishna Upadrasta IIT Hyderabad, Jyothi Vedurada IIT Hyderabad
14:00
30m
Talk
NEAT: A Benchmark for Indirect Control Flow Recovery
SAS
Tullis Nelson Auburn University, Tod Amon Sandia National Laboratories, Samuel Mulder Auburn University, Enoch Yang Auburn University, Raisul Arefin Nahid Auburn University, Douglas Ghormley Sandia National Laboratories, Timothy Loffredo Sandia National Laboratories, Kevan Baker Auburn University, Dylan Stancil Auburn University, Marshall Nelson Auburn University
14:30
30m
Talk
Inferring Empirical Sound Resource Bounds via Symbolic Execution and Linear Programming
SAS
Samuel Frontull University of Innsbruck, Manuel Meitinger University of Innsbruck, Georg Moser University of Innsbruck
15:30 - 17:00
Synthesis & Business MeetingSAS at Grand Ballroom Salons E+F+G+H
Chair(s): Aditya V. Thakur University of California at Davis, Sébastien Bardin CEA List - Université Paris-Saclay
15:30
30m
Talk
Synthesizing Parsing Expression Grammars via Analysis-based Pruning
SAS
Seongmin Ko Korea University, Jihyeok Park Korea University
16:00
60m
Meeting
Business Meeting and Radhia Cousot Award
SAS
Aditya V. Thakur University of California at Davis, Sébastien Bardin CEA List - Université Paris-Saclay

Thu 8 Oct

Displayed time zone: Pacific Time (US & Canada) change

08:30 - 10:00
Responsibility and DeterminismSAS at Grand Ballroom Salons E+F+G+H
Chair(s): Aditya V. Thakur University of California at Davis
09:00
30m
Talk
Making Responsibility Analysis Precise
SAS
Mila Dalla Preda University of Verona, Laura Canaia University of Verona, Italy
09:30
30m
Talk
Determinism Analysis and its Application to Evaluation Order Independence
SAS
10:30 - 12:00
Automated Repair and Vulnerability DetectionSAS at Grand Ballroom Salons E+F+G+H
Chair(s): Gagandeep Singh University of Illinois Urbana-Champaign
10:30
60m
Keynote
Automated Repair of Pluggable Type Checker Warnings
SAS
K: Manu Sridharan University of California at Riverside
11:30
30m
Talk
TriVul: Improving Precision of Static Vulnerability Detection through Multi-Agent Reasoning
SAS
Xinye Zhao University of Notre Dame, Joanna C. S. Santos University of Notre Dame
13:30 - 15:00
Learning for Analysis & Neural Network VerificationSAS at Grand Ballroom Salons E+F+G+H
Chair(s): Roberto Giacobazzi University of Arizona
13:30
30m
Talk
Heurix: A Framework to Automatically Learn Heuristics for Abstract Interpretation
SAS
Maykel Mattar Université Paris-Saclay, CEA, List / Université Bretagne Sud, IRISA, Michele Alberti Université Paris-Saclay, CEA, List, Valentin Perrelle Université Paris-Saclay, CEA, List, Palaiseau, France, Salah Sadou IRISA & CNRS, Universite Bretagne Sud,France
14:00
30m
Talk
Uncovering the Limits of Proof Sharing for Neural Networks
SAS
Kanak Das University of California, Riverside, Shubham Ugare University of Illinois Urbana-Champaign / Meta, Bor-Yuh Evan Chang University of Colorado Boulder; Amazon, Sasa Misailovic University of Illinois Urbana-Champaign, Gagandeep Singh University of Illinois Urbana-Champaign, Manu Sridharan University of California at Riverside
14:30
30m
Talk
NEAT: The Luna Bound Propagator for Formal Analysis of Neural Networks
SAS
Henry LeCates Amherst College, Haoze Wu Amherst College
15:30 - 17:00
Future Trends in Static AnalysisSAS at Grand Ballroom Salons E+F+G+H
Chair(s): Aditya V. Thakur University of California at Davis
15:30
5m
Talk
Analysis of Program Analysis
SAS
Roberto Giacobazzi University of Arizona
15:35
5m
Talk
Synthesizing Adaptive and Scalable Abstract Interpreters
SAS
Gagandeep Singh University of Illinois Urbana-Champaign
15:40
5m
Talk
Static Analysis with a Pause: The Case for Analyses That Finish at Runtime
SAS
Manas Thakur IIT Bombay
15:45
5m
Talk
Towards Sound Interactive Static Analysis
SAS
Michael Schwarz National University of Singapore
15:50
5m
Talk
Towards Cumulative Abstract Semantics
SAS
Bor-Yuh Evan Chang University of Colorado Boulder; Amazon
15:55
5m
Talk
Proof Engineering with LLMs and Auto-active Verifiers
SAS
Jenna DiVincenzo (Wise) Purdue University
16:00
5m
Talk
A Static Analysis Portfolio to Guide LLM-Based Code Repair
SAS
Laura Titolo Code Metal
16:05
5m
Talk
Toward Static Analysis of Natural-Language Specifications
SAS
Hakjoo Oh Korea University
16:10
50m
Panel
Future Trends in Static Analysis
SAS
P: Hakjoo Oh Korea University, P: Bor-Yuh Evan Chang University of Colorado Boulder; Amazon, P: Laura Titolo Code Metal, P: Michael Schwarz National University of Singapore, P: Manu Sridharan University of California at Riverside, P: Roberto Giacobazzi University of Arizona, P: Manas Thakur IIT Bombay, P: Gagandeep Singh University of Illinois Urbana-Champaign, P: Jenna DiVincenzo (Wise) Purdue University

Accepted Papers

Title
A Lattice of Union-Finds
SAS
A Modular Framework for Stack-Heap and Value Abstractions
SAS
Determinism Analysis and its Application to Evaluation Order Independence
SAS
FINDUS: Static Detection of Use-After-Scope Violations for Multi-threaded Programs
SAS
Generator-Dense Galois Connections
SAS
GPU-Accelerated Host-Aware Dead-Measurement Detection in Hybrid Quantum--Classical Programs
SAS
Heurix: A Framework to Automatically Learn Heuristics for Abstract Interpretation
SAS
Inferring Empirical Sound Resource Bounds via Symbolic Execution and Linear Programming
SAS
Making Responsibility Analysis Precise
SAS
NEAT: A Benchmark for Indirect Control Flow Recovery
SAS
NEAT: Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysis
SAS
NEAT: The Luna Bound Propagator for Formal Analysis of Neural Networks
SAS
PEG for information flow: analysis and incremental reasoning
SAS
Relaxed Residuation Theory - From Inversion to Abstract Interpretation beyond Classical Adjunctions
SAS
Rocq Bottom: Beyond Soundness with Precise Reasoning about Analysis Precision
SAS
Shape Abstraction of Thread Interferences
SAS
Synthesizing Parsing Expression Grammars via Analysis-based Pruning
SAS
TriVul: Improving Precision of Static Vulnerability Detection through Multi-Agent Reasoning
SAS
Uncovering the Limits of Proof Sharing for Neural Networks
SAS
Verifying ε-Differential Privacy Bit by Bit
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 2026 will consist of invited lectures and presentations of refereed papers. Contributions are welcomed on all aspects of program 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

Apart from the above topics, SAS 2026 welcomes papers in two special topics:

  1. Static Analysis and AI: Focusing on the application of static analyzers to enhance Code LLMs and Coding Agents, and conversely, the utilization of Code LLMs and Coding Agents to improve static analyzers.
  2. Static Analysis and Education: Covering tools and techniques for teaching static analysis to undergraduate and graduate students, and strategies for incorporating static analysis into CS education, particularly in lower-division undergraduate courses.

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 2026 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 2026 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.