- If you are a speaker, please check the SPLASH instructions for presenters.
- If you are a session chair, please check the SPLASH instructions for session chairs.
- The papers are linked from the program.
- Paper artifacts are availble at Zenodo.
- The proceedings are now available from Springer.
Please note that you have to reach them from this link to have access.
Sun 22 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | Session 1SAS 2023 at Room I Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
09:00 5m | Opening SAS 2023 Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, José Morales IMDEA Software Institute Pre-print | ||
09:05 60mKeynote | Goal-Directed Abstract Interpretation and Event-Driven FrameworksKeynote SAS 2023 Pre-print | ||
10:05 30mTalk | A Product of Shape and Sequence Abstractions (Radhia Cousot Young Researcher Best Paper Award) SAS 2023 Josselin Giet Ecole Normale Supérieure, Félix Ridoux Univ Rennes / IMDEA Software Institute, Xavier Rival Inria; ENS; CNRS; PSL University Pre-print |
10:30 - 11:00 | |||
11:00 - 12:30 | Domain precisionSAS 2023 at Room I Chair(s): Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon | ||
11:00 30mTalk | How fitting is your abstract domain? SAS 2023 Roberto Giacobazzi University of Arizona, Isabella Mastroeni University of Verona, Italy, Elia Perantoni University of Verona Pre-print | ||
11:30 30mTalk | Domain Precision in Galois Connection-less Abstract Interpretation SAS 2023 Pre-print | ||
12:00 30mTalk | A Formal Framework to Measure the Incompleteness of Abstract Interpretations SAS 2023 Marco Campion INRIA & École Normale Supérieure | Université PSL, Caterina Urban Inria & École Normale Supérieure | Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona Pre-print |
12:30 - 14:00 | |||
14:00 - 15:30 | |||
14:00 30mTalk | Generalized Program Sketching by Abstract Interpretation and Logical Abduction SAS 2023 Aleksandar S. Dimovski Mother Teresa University, Skopje Pre-print File Attached | ||
14:30 30mTalk | Reverse Template Processing using Abstract Interpretation SAS 2023 Matthieu Lemerre Université Paris-Saclay - CEA LIST Pre-print | ||
15:00 30mTalk | BREWasm: A General Static Binary Rewriting Framework for WebAssemblyRemote SAS 2023 Shangtong Cao Beijing University of Posts and Telecommunications, Ningyu He Peking University, Yao Guo Peking University, Haoyu Wang Huazhong University of Science and Technology Pre-print |
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 30mTalk | Quantum Constant Propagation SAS 2023 Yanbin Chen TUM School of Computation, Information and Technology, Technical University of Munich, Yannick Stade TUM School of Computation, Information and Technology, Technical University of Munich Pre-print | ||
16:30 30mTalk | Boosting Multi-Neuron Convex Relaxation for Neural Network Verification SAS 2023 Pre-print |
Mon 23 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 60mKeynote | Abstract Interpretation in Industry - Experience and Lessons LearnedKeynote SAS 2023 Pre-print | ||
10:00 30mTalk | Lifting On-Demand Analysis to Higher-Order Languages SAS 2023 Daniel Schoepe Amazon, David Seekatz Unaffiliated, Ilina Stoilkovska Amazon, Sandro Stucki Amazon, Daniel Tattersall Amazon, Pauline Bolignano Amazon, Franco Raimondi Amazon, Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon Link to publication Pre-print |
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 30mTalk | Symbolic transformation of expressions in modular arithmetic SAS 2023 Pre-print | ||
11:30 30mTalk | Polynomial Analysis of Modular Arithmetic SAS 2023 Pre-print | ||
12:00 30mTalk | Octagons Revisited - Elegant Proofs and Simplified Algorithms SAS 2023 Pre-print |
12:30 - 14:00 | |||
14:00 - 15:30 | |||
14:00 30mTalk | Error Invariants for Fault Localization via Abstract Interpretation SAS 2023 Aleksandar S. Dimovski Mother Teresa University, Skopje Pre-print File Attached | ||
14:30 30mTalk | Error Localization for Sequential Effect Systems SAS 2023 Link to publication Pre-print | ||
15:00 30mTalk | Scaling up Roundoff Analysis of Functional Data Structure Programs SAS 2023 Pre-print |
15:30 - 16:00 | |||
16:00 - 17:30 | Session 8SAS 2023 at Room I Chair(s): José Morales IMDEA Software Institute, Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute | ||
16:00 60mKeynote | Building Trust and Safety in Artificial Intelligence with Abstract InterpretationRemoteKeynote SAS 2023 Pre-print | ||
17:00 30mAwards | Radhia Cousot Award and PC report SAS 2023 C: Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, C: José Morales IMDEA Software Institute |
Tue 24 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | Cost/precision trade-offs and accelerationSAS 2023 at Room I Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University | ||
09:00 30mTalk | ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses SAS 2023 Pre-print | ||
09:30 30mTalk | Unconstrained Variable Oracles for Faster Static Analyses SAS 2023 Vincenzo Arceri University of Parma, Italy, Greta Dolcetti University of Parma - Department of Mathematical, Physical, and Computer Sciences, Enea Zaffanella University of Parma, Italy Pre-print | ||
10:00 30mTalk | Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs SAS 2023 Pre-print |
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 60mKeynote | Verifying Infinitely Many Programs at OnceKeynote SAS 2023 Pre-print | ||
12:00 30mTalk | Mutual Refinements of Context-Free Language Reachability SAS 2023 Pre-print |
12:30 - 14:00 | |||
Accepted Papers
Call for Papers
Are you running late in preparing your SAS paper? No worries! Due to popular demand we are continuing to accept papers (not just updates) until the May 1 full paper deadline!"
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 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)
- Full paper submission:
April 24, 2023 abstractsPapers accepted (not just updates) until May 1 - Artifact submission: May 6, 2023
- Author response period: June 11-14, 2023
- Notification: June 29, 2023
- Final version due: August 3, 2023
- Conference: Part of SPLASH, Oct 22-24, 2023
Topics
The technical program for SAS 2023 will consist of invited lectures and presentations of refereed papers. Contributions are welcomed on all aspects of static 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
Paper Submission
All paper submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity.
Submission link: https://easychair.org/conferences/?conf=sas2023
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
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 experience papers, all other papers will follow a lightweight double-blind reviewing process. The identity of the authors for the remaining papers will be known to the reviewers.
Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic, object-oriented, aspect, multi-core, distributed, and GPU programming.
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.
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.
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 2023 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.
Results (72)
Vincenzo ArceriArceri, Vincenzo University of Parma, ItalyItaly |
Jérôme BoillotBoillot, Jérôme École Normale Supérieure, PSL University & INRIAFrance |
Pauline BolignanoBolignano, Pauline AmazonUnited Kingdom |
Shangtong CaoCao, Shangtong Beijing University of Posts and TelecommunicationsChina |
Bor-Yuh Evan ChangChang, Bor-Yuh Evan University of Colorado at Boulder; AmazonUnited States |
Liqian ChenChen, Liqian National University of Defense Technology, ChinaChina |
Yanbin ChenChen, Yanbin TUM School of Computation, Information and Technology, Technical University of MunichGermany |
Yu-Fang ChenChen, Yu-Fang Academia SinicaTaiwan |
Chris CoppinsCoppins, Chris University of KentUnited Kingdom |
Patrick CousotCousot, Patrick |
Mila Dalla PredaDalla Preda, Mila University of VeronaItaly |
Eva DarulovaDarulova, Eva Uppsala UniversitySweden |
Shuo DingDing, Shuo Georgia Institute of TechnologyUnited States |
Greta DolcettiDolcetti, Greta University of Parma - Department of Mathematical, Physical, and Computer SciencesItaly |
Neil EvansEvans, Neil AWEUnited Kingdom |
Pietro FerraraFerrara, Pietro Università Ca' Foscari, Venezia, ItalyItaly |
Florian FrohnFrohn, Florian RWTH Aachen UniversityGermany |
Jürgen GieslGiesl, Jürgen RWTH Aachen UniversityGermany |
Josselin GietGiet, Josselin Ecole Normale SupérieureFrance |
Colin GordonGordon, Colin Drexel UniversityUnited States |
Roberta GoriGori, Roberta University of PisaItaly |
Yao GuoGuo, Yao Peking UniversityChina |
Manuel HermenegildoHermenegildo, Manuel Technical University of Madrid (UPM) and IMDEA Software InstituteSpain |
Andy KingKing, Andy KentUnited Kingdom |
Jiaxiang LiuLiu, Jiaxiang Shenzhen UniversityChina |
Francesco LogozzoLogozzo, Francesco FacebookUnited States |
Antoine MinéMiné, Antoine Sorbonne UniversitéFrance |
José MoralesMorales, José IMDEA Software InstituteSpain |
Jorge A. NavasNavas, Jorge A. CertoraUnited States |
Elia PerantoniPerantoni, Elia University of VeronaItaly |
Félix RidouxRidoux, Félix Univ Rennes / IMDEA Software InstituteFrance |
Martin C. RinardRinard, Martin C. Massachusetts Institute of TechnologyUnited States |
Xavier RivalRival, Xavier Inria; ENS; CNRS; PSL UniversityFrance |
Daniel SchoepeSchoepe, Daniel AmazonUnited Kingdom |
Michael SchwarzSchwarz, Michael Technische Universität MünchenGermany |
Thomas SeedSeed, Thomas University of KentUnited Kingdom |
David SeekatzSeekatz, David UnaffiliatedCanada |
Helmut SeidlSeidl, Helmut Technische Universität MünchenGermany |
Mihaela SighireanuSighireanu, Mihaela IRIF, Université Paris Diderot, FranceFrance |
Gagandeep SinghSingh, Gagandeep University of Illinois at Urbana-Champaign; VMware ResearchUnited States |
Fu SongSong, Fu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, and University of Chinese Academy of Sciences Beijing, ChinaChina |
Yannick StadeStade, Yannick TUM School of Computation, Information and Technology, Technical University of MunichGermany |
Ilina StoilkovskaStoilkovska, Ilina AmazonUnited Kingdom |
Sandro StuckiStucki, Sandro AmazonSweden |
Yulei SuiSui, Yulei UNSWAustralia |
Daniel TattersallTattersall, Daniel AmazonUnited States |
Laura TitoloTitolo, Laura NIA/NASA LaRCUnited States |
Qirun ZhangZhang, Qirun Georgia Institute of TechnologyUnited States |
Xin ZhangZhang, Xin Peking UniversityChina |
Ye ZhengZheng, Ye Shenzhen UniversityChina |