Welcome to the website of the 31st Static Analysis Symposium (SAS 2024). 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.

SAS’24 will take place from Sunday, October 20th to Tuesday, October 22nd, 2024.

This year, at SAS’24, the Radhia Cousot Award will be announced at the conference! The award is in memory of Radhia Cousot and her fundamental contributions to static analysis. All young researchers (students and post-doc) authors of papers accepted at SAS’24 are invited to join SAS and register at the conference.

Keynote Speakers

Supporters
Gold
Silver
Silver
Bronze
Bronze
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

Sun 20 Oct

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

09:00 - 10:30
Modularity and Memory AnalysisSAS at San Gabriel
Chair(s): Roberto Giacobazzi University of Arizona
09:00
60m
Keynote
Static Analysis Sparsity and Modularity
SAS
Kwangkeun Yi Seoul National University
10:00
30m
Under-approximating Memory Abstractions
SAS
Marco Milanese Sorbonne University, Antoine Miné Sorbonne Université
Pre-print
10:30 - 11:00
Coffee BreakCatering at Foyer
10:30
30m
Coffee break
Break
Catering

11:00 - 12:30
Types, Control-flow and trace partitioningSAS at San Gabriel
Chair(s): Michele Pasqua University of Verona
11:00
30m
Full-paper
BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code
SAS
Ian Smith Trail of Bits
Pre-print
11:30
30m
Full-paper
Full Control-Flow Sensitivity for Definitional Interpreters
SAS
Kimball Germane Brigham Young University
12:00
30m
Full-paper
Trace Partitioning as an Optimization Problem
SAS
Charles Babu M CEA-List, Matthieu Lemerre Université Paris-Saclay - CEA LIST, Sébastien Bardin CEA LIST, University Paris-Saclay, Jean-Yves Marion LORIA
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

14:00 - 15:30
Machine learning and Neural networksSAS at San Gabriel
Chair(s): Marco Campion INRIA & École Normale Supérieure | Université PSL
14:00
60m
Tutorial
Abstract Interpretation-Based Certification of Hyperproperties for High-Stakes Machine Learning Software
SAS
Caterina Urban Inria & École Normale Supérieure | Université PSL
15:00
30m
Full-paper
Robustness Verification of Multi-Label Neural Network Classifiers
SAS
15:30 - 16:00
Coffee BreakCatering at Foyer
15:30
30m
Coffee break
Break
Catering

16:00 - 17:30
Machine Learning and Neural networksSAS at San Gabriel
Chair(s): Marco Campion INRIA & École Normale Supérieure | Université PSL
16:00
30m
Full-paper
Abstract Interpretation of ReLU Neural Networks with Optimizable Polynomial Relaxations
SAS
Philipp Kern Karlsruhe Institute of Technology (KIT), Carsten Sinz Karlsruhe Institute of Technology
16:30
30m
Short-paper
ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses (NEAT paper)
SAS
Avaljot Singh , Yasmin Sarita Cornell University, Charith Mendis University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research

Mon 21 Oct

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

09:00 - 10:30
Authorisation and responsibilitySAS at San Gabriel
Chair(s): Sébastien Bardin CEA LIST, University Paris-Saclay
09:00
60m
Tutorial
A New Language for Expressive, Fast, Safe, and Analyzable Authorization
SAS
Emina Torlak Amazon Web Services, USA
10:00
30m
Full-paper
On the Role of Cognizance in Responsibility
SAS
Laura Canaia , Mila Dalla Preda University of Verona
10:30 - 11:00
Coffee BreakCatering at Foyer
10:30
30m
Coffee break
Break
Catering

11:00 - 12:30
Verification cost and quantitative analysisSAS at San Gabriel
11:00
30m
Full-paper
Verification of programs with ADTs using Shallow Horn Clauses
SAS
Théo Losekoot , Thomas Genet IRISA, Univ Rennes, Thomas P. Jensen INRIA Rennes
11:30
30m
Full-paper
An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants
SAS
Louis Rustenholz Universidad Politécnica de Madrid (UPM) and IMDEA Software Institute, Pedro López-García IMDEA Software Institute, José Morales IMDEA Software Institute, Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute
Link to publication Pre-print
12:00
30m
Full-paper
Quantitative Static Timing Analysis
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Marco Campion INRIA & École Normale Supérieure | Université PSL, Caterina Urban Inria & École Normale Supérieure | Université PSL
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

14:00 - 15:30
Quantum and system level analysisSAS at San Gabriel
Chair(s): Qirun Zhang Georgia Institute of Technology
14:00
30m
Short-paper
Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel (NEAT paper)
SAS
Pre-print
14:30
30m
Full-paper
Static Analysis of Quantum Programs
SAS
Nicola Assolini Università degli Studi di Verona, Alessandra Di Pierro University of Verona, Italy, Isabella Mastroeni University of Verona, Italy
15:00
30m
Short-paper
Verifying components of Arm® Confidential Computing Architecture with ESBMC (NEAT paper)
SAS
Tong Wu , Shale Xiong ARM, Edoardo Manino , Gareth Stockwell ARM, Lucas C. Cordeiro University of Manchester, UK and Federal University of Amazonas, Brazil
15:30 - 16:00
Coffee BreakCatering at Foyer
15:30
30m
Coffee break
Break
Catering

16:00 - 17:30
Radhia Cousot Award and SAS24 Business MeetingSAS at San Gabriel
Chair(s): Marco Campion INRIA & École Normale Supérieure | Université PSL, Roberto Giacobazzi University of Arizona, Alessandra Gorla IMDEA Software Institute
16:00
60m
Meeting
Radhia Cousot Award and Business Meeting
SAS

Tue 22 Oct

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

09:00 - 10:30
Automatising Program AnalysisSAS at San Gabriel
09:00
60m
Keynote
TBA
SAS
Mayur Naik University of Pennsylvania
10:00
30m
Full-paper
Synthesizing Abstract Transformers for Reduced-Product Domains
SAS
Pankaj Kumar Kalita IIT Kanpur, Thomas Reps University of Wisconsin-Madison, Subhajit Roy IIT Kanpur
10:30 - 11:00
Coffee BreakCatering at Foyer
10:30
30m
Coffee break
Break
Catering

11:00 - 12:30
Tracing bugs and flawsSAS at San Gabriel
Chair(s): Aditya V. Thakur University of California at Davis
11:00
60m
Keynote
Measuring data lineage
SAS
12:00
30m
Full-paper
Lift-offline: Instruction Lifter Generators
SAS
Nicholas Coughlin Defence Science and Technology Group, Australia, Alistair Michael , Kait Lam
12:30 - 14:00
12:30
90m
Lunch
Lunch
Catering

15:30 - 16:00
Coffee BreakCatering at Foyer
15:30
30m
Coffee break
Break
Catering

Accepted Papers

Title
Abstract Interpretation of ReLU Neural Networks with Optimizable Polynomial Relaxations
SAS
An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants
SAS
Link to publication Pre-print
BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code
SAS
Pre-print
ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses (NEAT paper)
SAS
Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel (NEAT paper)
SAS
Pre-print
Full Control-Flow Sensitivity for Definitional Interpreters
SAS
GoGuard: Efficient Static Blocking Bug Detection for Go
SAS
Lift-offline: Instruction Lifter Generators
SAS
On the Role of Cognizance in Responsibility
SAS
Quantitative Static Timing Analysis
SAS
Robustness Verification of Multi-Label Neural Network Classifiers
SAS
Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler (NEAT paper)
SAS
File Attached
Static Analysis of Quantum Programs
SAS
Synthesizing Abstract Transformers for Reduced-Product Domains
SAS
Trace Partitioning as an Optimization Problem
SAS
Under-approximating Memory Abstractions
SAS
Pre-print
Verification of programs with ADTs using Shallow Horn Clauses
SAS
Verifying components of Arm® Confidential Computing Architecture with ESBMC (NEAT paper)
SAS

Call for Papers

Deadlines extended! Check out the new dates!

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.

Important Dates (All deadlines are AoE (Anywhere on Earth))

  • Paper submission: Sunday, May 5th, Sunday May 19th, 2024 (Extended Deadline)
  • Artifact submission: Sunday, May 12th, Wednesday May 22nd, 2024 (Extended Deadline)
  • Author response: Monday, June 17th - Wednesday, June 19th, Thursday, June 27th - Sunday, June 30th, 2024
  • Notification: Sunday, July 7th, Tuesday, July 16th, 2024
  • Camera ready: Monday, August 5th, Monday, August 12th, 2024

Topics

The technical program for SAS 2024 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
All paper submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity.

Submission link: https://easychair.org/conferences/?conf=sas24

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
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 lightweight 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 2024 Artifacts page.

Submission Details

Lightweight Double-Blind Requirement

All regular papers will follow a double-blind process, where author names and affiliations are hidden for initial review. Author names will be revealed to a reviewer only after their review has been submitted. 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. Authors should feel free to disseminate their ideas or draft versions of their papers as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas.

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

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 static program analysis. By becoming a SAS24 supporter, your organisation can reach a highly qualified technical audience of academics, industrial researchers, engineers, and students active in this fundamental area. You will be able to increase your visibility and product awareness among the people who are the most knowledgeable and passionate about your products.

All supporters will receive recognition of their level of contribution in print, on the web, in registration brochures, in the conference program, and during opening and closing of the conference.

You can support SAS24 at the following sponsorship levels:

  • Gold ($2.5k and up)
    • Company-provided banner during the conference;
    • Exhibit space at the conference;
    • May supply giveaways or swags;
    • Logo or name visibility (web, print, email, on-site);
    • 2 conference registrations included;
    • Acknowledgement during opening and closing remarks
  • Silver ($2k)
    • Logo or name visibility (web, print, email, on-site)
    • May supply giveaways or swags
    • 1 conference registrations included
    • Acknowledgement during opening and closing remarks
  • Bronze ($1k)
    • Logo or name visibility (web, print, email, on-site)
    • May supply giveaways or swags
    • Acknowledgement during opening and closing remarks
In addition to the four sponsorship levels and their benefits above, sponsors can support student travel award: $2K each!
Questions? Use the SAS contact form.