SAS 2022
Mon 5 - Wed 7 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Dates
Tracks
Plenary
You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

09:00 - 10:00
Keynote 1SAS at AMRF Auditorium
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign, Caterina Urban Inria & École Normale Supérieure | Université PSL
09:00
60m
Keynote
Commercial-Grade Static Analyzers in DatalogIn PersonKeynote
SAS
Bernhard Scholz University of Sydney
10:00 - 10:30
10:00
30m
Coffee break
Coffee break
SPLASH Catering and Social Events

10:30 - 12:00
Model Checking and VerificationSAS at AMRF Auditorium
Chair(s): Arlen Cox IDA
10:30
30m
Talk
Parameterized Recursive Refinement Types for Automated Program Verification
SAS
Ryoya Mukai The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan
11:00
30m
Talk
Efficient Modular SMT-Based Model Checking of Pointer ProgramsVirtual
SAS
Isabel Garcia-Contreras University of Waterloo, Arie Gurfinkel University of Waterloo, Jorge A. Navas Certora, inc.
11:30
30m
Talk
Case Study on Verification-Witness Validators: Where We Are and Where We Go
SAS
Dirk Beyer LMU Munich, Jan Strejcek Masaryk University
Link to publication DOI Media Attached
12:00 - 13:30
12:00
90m
Lunch
Lunch
SPLASH Catering and Social Events

13:30 - 15:00
Numerical Static AnalysesSAS at AMRF Auditorium
Chair(s): Isabella Mastroeni University of Verona, Italy
13:30
30m
Talk
CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial AttacksVirtual
SAS
Zhe Zhao ShanghaiTech University, Yedi Zhang ShanghaiTech University, Guangke Chen ShanghaiTech University, Fu Song ShanghaiTech University, Taolue Chen Birkbeck University of London, Jiaxiang Liu Shenzhen University
14:00
30m
Talk
Boosting Robustness Verification of Semantic Feature Neighborhoods
SAS
Anan Kabaha Technion, Israel Institute of Technology, Dana Drachsler Cohen Technion
14:30
30m
Talk
Lifting Numeric Relational Domains to Algebraic Data Types
SAS
Santiago Bautista Univ Rennes, Inria, CNRS, IRISA, Thomas P. Jensen INRIA Rennes, Benoît Montagu Inria
Pre-print File Attached
15:00 - 15:30
15:00
30m
Coffee break
Coffee break
SPLASH Catering and Social Events

15:30 - 17:00
Keynote 2, Radhia Cousot Award, PC Chairs ReportSAS at AMRF Auditorium
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign, Caterina Urban Inria & École Normale Supérieure | Université PSL
15:30
60m
Keynote
Logical Reasoning in Reinforcement Learning: A Boon or Bane? KeynoteVirtual
SAS
Suguman Bansal Rice University, USA
16:30
10m
Awards
Radhia Cousot Award
SAS
Caterina Urban Inria & École Normale Supérieure | Université PSL, Gagandeep Singh University of Illinois at Urbana-Champaign
16:40
20m
Day closing
PC Chairs Report
SAS
Caterina Urban Inria & École Normale Supérieure | Université PSL, Gagandeep Singh University of Illinois at Urbana-Champaign

Tue 6 Dec

Displayed time zone: Auckland, Wellington change

09:00 - 10:00
Keynote 3SAS at AMRF Auditorium
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign, Caterina Urban Inria & École Normale Supérieure | Université PSL
09:00
60m
Keynote
Towards Efficient Reasoning of Quantum ProgramsKeynote
SAS
Nengkun Yu Stony Brook University, USA
10:00 - 10:30
10:00
30m
Coffee break
Coffee break
SPLASH Catering and Social Events

10:30 - 12:00
SecuritySAS at AMRF Auditorium
Chair(s): Emanuele D’Osualdo MPI-SWS
10:30
30m
Talk
SecWasm: Information Flow Control for WebAssemblyVirtual
SAS
Iulia Bastys Chalmers University of Technology, Maximilian Algehed Chalmers University of Technology, Sweden, Alexander Sjösten TU Wien, Andrei Sabelfeld Chalmers University of Technology
11:00
30m
Talk
Adversarial Logic
SAS
Julien Vanegue Bloomberg
11:30
30m
Talk
Property-driven code obfuscations - Reinterpreting Jones-optimality in Abstract Interpretation
SAS
Roberto Giacobazzi University of Verona, Isabella Mastroeni University of Verona, Italy
13:30 - 15:00
Logic and CompletenessSAS at AMRF Auditorium
Chair(s): Roberto Giacobazzi University of Verona
13:30
30m
Talk
Invariant Inference With Provable Complexity From the Monotone Theory
SAS
Yotam M. Y. Feldman Tel Aviv University, Sharon Shoham Tel Aviv University
14:00
30m
Talk
Local Completeness Logic on Kleene Algebra with Tests
SAS
Marco Milanese Dipartimento di Matematica, University of Padova, Italy, Francesco Ranzato University of Padova
14:30
30m
Talk
Deciding program properties via complete abstractions on bounded domains
SAS
Roberto Bruni University of Pisa, Roberta Gori University of Pisa, Nicolas Manini IMDEA Software Institute
15:00 - 15:30
15:00
30m
Coffee break
Coffee break
SPLASH Catering and Social Events

15:30 - 17:00
Invariant and Program SynthesisSAS at AMRF Auditorium
Chair(s): Subhajit Roy IIT Kanpur
15:30
30m
Talk
Bootstrapping Library-Based Synthesis
SAS
Kangjing Huang Purdue University, USA, Xiaokang Qiu Purdue University, USA
16:00
30m
Talk
Automated Synthesis of Asynchronizations
SAS
Sidi Mohamed Beillahi University of Toronto, Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea Ecole Polytechnique / LIX / CNRS, Shuvendu K. Lahiri Microsoft Research
16:30
30m
Talk
Solving Invariant Generation for Unsolvable Loops
SAS

Wed 7 Dec

Displayed time zone: Auckland, Wellington change

10:00 - 10:30
10:00
30m
Coffee break
Coffee break
SPLASH Catering and Social Events

10:30 - 12:00
Compilers and OptimizationsSAS at AMRF Auditorium
10:30
30m
Talk
Semantic Foundations for Cost Analysis of Pipeline-Optimized ProgramsVirtual
SAS
Solène Mirliaz ENS Rennes / IRISA / Inria, David Pichardie Meta, Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Adrien Koutsos INRIA Paris, Peter Schwabe Max Planck Institute for Security and Privacy
11:00
30m
Talk
Principles of Staged Static+Dynamic Partial Analysis
SAS
Aditya Anand IIT Mandi, Manas Thakur IIT Bombay
11:30
30m
Talk
Fast and incremental computation of weak control closure
SAS
Abu Naser Masud Malardalen University
12:00 - 13:30
12:00
90m
Lunch
Lunch
SPLASH Catering and Social Events

Accepted Papers

Title
Adversarial Logic
SAS
Automated Synthesis of Asynchronizations
SAS
Boosting Robustness Verification of Semantic Feature Neighborhoods
SAS
Bootstrapping Library-Based Synthesis
SAS
Case Study on Verification-Witness Validators: Where We Are and Where We Go
SAS
Link to publication DOI Media Attached
CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial AttacksVirtual
SAS
Deciding program properties via complete abstractions on bounded domains
SAS
Efficient Modular SMT-Based Model Checking of Pointer ProgramsVirtual
SAS
Fast and incremental computation of weak control closure
SAS
Invariant Inference With Provable Complexity From the Monotone Theory
SAS
Lifting Numeric Relational Domains to Algebraic Data Types
SAS
Pre-print File Attached
Local Completeness Logic on Kleene Algebra with Tests
SAS
Parameterized Recursive Refinement Types for Automated Program Verification
SAS
Principles of Staged Static+Dynamic Partial Analysis
SAS
Property-driven code obfuscations - Reinterpreting Jones-optimality in Abstract Interpretation
SAS
SecWasm: Information Flow Control for WebAssemblyVirtual
SAS
Semantic Foundations for Cost Analysis of Pipeline-Optimized ProgramsVirtual
SAS
Solving Invariant Generation for Unsolvable Loops
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 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: Wednesday, May 4th, 2022

Are you running late in preparing your paper? No worries! Submit what you have by May 4th and you will have one extra week until May 11th for updating your paper.

  • Artifact submission: May 18, 2022 AoE May 25th, 2022 AoE

  • Author response period: Monday, June 27th, 2022 - Thursday, June 30th, 2022

  • Notification: Friday, July 15th, 2022
  • Camera ready version due: Friday, September 16th, 2022

Topics

The technical program for SAS 2022 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 Submissions

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

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

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. All regular 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 the 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

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.

Questions? Use the SAS contact form.