SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021

Welcome to the 28th Static Analysis Symposium (SAS 2021)!

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.


SAS begins this Sunday! We are looking forward to inspirational talks and enjoyable discussions! Please join us.

The SAS proceedings is now available, with free access for 4 months.


We are very happy to announce that this year’s Radhia Cousot Award goes to Tianhan Lu (University of Colorado, Boulder, CO, USA) for the paper “Selectively-Amortized Resource Bounding” (with Bor-Yuh Evan Chang and Ashutosh Trivedi). Congratulations!!


We would like to thank Springer and Facebook for their sponsorship. Facebook will also sponsor the invited talk by Prof. Mooly Sagiv.

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

Sun 17 Oct

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

09:00 - 10:20
Session 1ASAS at Zurich B +8h
Chair(s): Cezara Drăgoi Inria / ENS / Informal Systems
09:00
15m
Talk
Accelerating Program Analyses in Datalog by Merging Library FactsVirtual
SAS
Yifan Chen Peking University, Chenyang Yang , Xin Zhang Peking University, Yingfei Xiong Peking University, Hao Tang Peking University, Xiaoyin Wang University of Texas at San Antonio, Lu Zhang Peking University
09:15
15m
Talk
Exploiting Verified Neural Networks via Floating Point Numerical ErrorVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard
Pre-print
09:30
15m
Talk
Verifying Low-dimensional Input Neural Networks via Input QuantizationVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology
Pre-print
09:45
15m
Talk
A Multi-Language Static Analysis of Python Programs with Native C ExtensionsVirtual
SAS
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Pre-print Media Attached
10:00
20m
Live Q&A
Session 1A Discussion, Questions and Answers Virtual
SAS

13:50 - 15:10
Session 3ASAS at Zurich B +8h
Chair(s): Mihaela Sighireanu IRIF, Université Paris Diderot, France
13:50
15m
Talk
Static Analysis of Endian Portability by Abstract InterpretationVirtual
SAS
David Delmas Airbus & Sorbonne Université, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
14:05
15m
Talk
Verified Functional Programming of an Abstract InterpreterVirtual
SAS
Lucas Franceschino INRIA, David Pichardie Facebook Paris, Jean-Pierre Talpin INRIA, France
14:30
15m
Talk
Data Abstraction: A General Framework to Handle Program Verification of Data StructuresVirtual
SAS
Julien Braine , Laure Gonnord University of Lyon & LIP, France, David Monniaux CNRS/VERIMAG
14:45
25m
Live Q&A
Session 3A Discussion, Questions and AnswersVirtual
SAS

17:00 - 18:20
Session 1ASAS at Zurich B
Chair(s): Kedar Namjoshi Nokia Bell Labs
17:00
15m
Talk
Accelerating Program Analyses in Datalog by Merging Library FactsVirtual
SAS
Yifan Chen Peking University, Chenyang Yang , Xin Zhang Peking University, Yingfei Xiong Peking University, Hao Tang Peking University, Xiaoyin Wang University of Texas at San Antonio, Lu Zhang Peking University
17:15
15m
Talk
Exploiting Verified Neural Networks via Floating Point Numerical ErrorVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard
Pre-print
17:30
15m
Talk
Verifying Low-dimensional Input Neural Networks via Input QuantizationVirtual
SAS
Kai Jia Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology
Pre-print
17:45
15m
Talk
A Multi-Language Static Analysis of Python Programs with Native C ExtensionsVirtual
SAS
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Pre-print Media Attached
18:00
20m
Live Q&A
Session 1A Discussion, Questions and Answers Virtual
SAS

Mon 18 Oct

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

07:40 - 09:00
Session 4BSAS at Zurich B
Chair(s): Antoine Miné Sorbonne Université
07:40
15m
Talk
Automated Verification of the Parallel Bellman--Ford AlgorithmVirtual
SAS
Mohsen Safari University of Twente, The Netherlands, Wytse Oortwijn ETH Zurich, Switzerland, Marieke Huisman University of Twente
07:55
15m
Talk
Backward Symbolic Execution with Loop FoldingVirtual
SAS
Marek Chalupa Masaryk University, Jan Strejcek Masaryk University
08:10
15m
Talk
Improving Thread-Modular Abstract InterpretationVirtual
SAS
Michael Schwarz Technische Universität München, Simon Saan University of Tartu, Estonia, Helmut Seidl Technische Universität München, Kalmer Apinis University of Tartu, Estonia, Julian Erhard , Vesal Vojdani University of Tartu
Pre-print Media Attached
08:25
15m
Talk
Symbolic Automatic Relations and Their Applications to SMT and CHC SolvingVirtual
SAS
Takumi Shimoda The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan
08:40
20m
Live Q&A
Session 4B Discussion, Questions and Answers
SAS

10:50 - 12:10
Session 2BSAS at Zurich B +8h
Chair(s): Cezara Drăgoi Inria / ENS / Informal Systems
10:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication AbstractionVirtual
SAS
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Arie Gurfinkel University of Waterloo, Jorge A. Navas SRI International, Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys
Pre-print
11:05
15m
Talk
Selectively-Amortized Resource BoundingVirtual
SAS
Tianhan Lu University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Ashutosh Trivedi
Pre-print
11:20
15m
Talk
Thread-modular Analysis of Release-Acquire ConcurrencyVirtual
SAS
Divyanjali Sharma IIT Delhi, India, Subodh Sharma IIT Delhi
11:35
35m
Live Q&A
Session 2B Discussion, Questions and Answers
SAS

13:50 - 15:10
Session 3BSAS at Zurich B
Chair(s): Kedar Namjoshi Nokia Bell Labs
13:50
80m
Keynote
Interactive Code AnalysisInvited TalkVirtual
SAS
I: Gerard Holzmann NASA/Caltech Jet Propulsion Laboratory
15:40 - 17:00
Session 4BSAS at Zurich B -8h
Chair(s): Kedar Namjoshi Nokia Bell Labs
15:40
15m
Talk
Automated Verification of the Parallel Bellman--Ford AlgorithmVirtual
SAS
Mohsen Safari University of Twente, The Netherlands, Wytse Oortwijn ETH Zurich, Switzerland, Marieke Huisman University of Twente
15:55
15m
Talk
Backward Symbolic Execution with Loop FoldingVirtual
SAS
Marek Chalupa Masaryk University, Jan Strejcek Masaryk University
16:10
15m
Talk
Improving Thread-Modular Abstract InterpretationVirtual
SAS
Michael Schwarz Technische Universität München, Simon Saan University of Tartu, Estonia, Helmut Seidl Technische Universität München, Kalmer Apinis University of Tartu, Estonia, Julian Erhard , Vesal Vojdani University of Tartu
Pre-print Media Attached
16:25
15m
Talk
Symbolic Automatic Relations and Their Applications to SMT and CHC SolvingVirtual
SAS
Takumi Shimoda The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan
16:40
20m
Live Q&A
Session 4B Discussion, Questions and Answers
SAS

18:50 - 20:10
Session 2BSAS at Zurich B
Chair(s): Suvam Mukherjee Microsoft Research
18:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication AbstractionVirtual
SAS
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Arie Gurfinkel University of Waterloo, Jorge A. Navas SRI International, Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys
Pre-print
19:05
15m
Talk
Selectively-Amortized Resource BoundingVirtual
SAS
Tianhan Lu University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Ashutosh Trivedi
Pre-print
19:20
15m
Talk
Thread-modular Analysis of Release-Acquire ConcurrencyVirtual
SAS
Divyanjali Sharma IIT Delhi, India, Subodh Sharma IIT Delhi
19:35
35m
Live Q&A
Session 2B Discussion, Questions and Answers
SAS

Tue 19 Oct

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

07:40 - 09:00
Session 4CSAS at Zurich D
Chair(s): Jerome Feret INRIA Paris
07:40
15m
Talk
Fast and Efficient Bit-Level Precision TuningVirtual
SAS
Assalé Adjé Université de Perpignan Via Domitia, Dorra Ben Khalifa Université de Perpignan Via Domitia, Matthieu Martel Université de Perpignan Via Domitia
07:55
15m
Talk
Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Caterina Urban INRIA & École Normale Supérieure | Université PSL
08:10
15m
Talk
Static analysis of ReLU neural networks with tropical polyhedraVirtual
SAS
Eric Goubault Ecole Polytechnique, Sebastien Palumby Ecole Polytechnique, Sylvie Putot École Polytechnique, Louis Rustenholz École Polytechnique, Sriram Sankaranarayanan University of Colorado, Boulder
08:25
15m
Talk
Toward Neural-Network-Guided Program Synthesis and VerificationVirtual
SAS
Naoki Kobayashi University of Tokyo, Japan, Taro Sekiyama National Institute of Informatics, Issei Sato The University of Tokyo, Hiroshi Unno University of Tsukuba
08:40
20m
Live Q&A
Session 4C Discussion, Questions and AnswersVirtual
SAS

10:50 - 12:10
Session 2CSAS at Zurich D
Chair(s): Cezara Drăgoi Inria / ENS / Informal Systems
10:50
80m
Talk
Pointer Analysis of Bytecode Programs for Effective Formal Verification of Smart ContractsInvited TalkVirtual
SAS
Mooly Sagiv Tel Aviv University
13:50 - 15:10
Session 3CSAS at Zurich D +8h
Chair(s): David Pichardie Facebook Paris
13:50
15m
Talk
Automatic Synthesis of Data-Flow AnalyzersVirtual
SAS
Xuezheng Xu UNSW Sydney, Xudong Wang UNSW Sydney, Jingling Xue UNSW Sydney
14:05
15m
Talk
Disjunctive Interval AnalysisVirtual
SAS
14:20
15m
Talk
Hash Consed Points-To SetsVirtual
SAS
Mohamad Barbar University of Technology Sydney; CSIRO’s Data61, Yulei Sui University of Technology Sydney
14:35
15m
Talk
Selective Context-Sensitivity for k-CFA with CFL-ReachabilityVirtual
SAS
Jingbo Lu UNSW Sydney, Dongjie He UNSW Sydney, Jingling Xue UNSW Sydney
14:50
20m
Live Q&A
Session 3C Discussion, Questions and Answers
SAS

15:40 - 17:00
Session 4CSAS at Zurich D -8h
Chair(s): Suvam Mukherjee Microsoft Research
15:40
15m
Talk
Fast and Efficient Bit-Level Precision TuningVirtual
SAS
Assalé Adjé Université de Perpignan Via Domitia, Dorra Ben Khalifa Université de Perpignan Via Domitia, Matthieu Martel Université de Perpignan Via Domitia
15:55
15m
Talk
Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Caterina Urban INRIA & École Normale Supérieure | Université PSL
16:10
15m
Talk
Static analysis of ReLU neural networks with tropical polyhedraVirtual
SAS
Eric Goubault Ecole Polytechnique, Sebastien Palumby Ecole Polytechnique, Sylvie Putot École Polytechnique, Louis Rustenholz École Polytechnique, Sriram Sankaranarayanan University of Colorado, Boulder
16:25
15m
Talk
Toward Neural-Network-Guided Program Synthesis and VerificationVirtual
SAS
Naoki Kobayashi University of Tokyo, Japan, Taro Sekiyama National Institute of Informatics, Issei Sato The University of Tokyo, Hiroshi Unno University of Tsukuba
16:40
20m
Live Q&A
Session 4C Discussion, Questions and AnswersVirtual
SAS

21:50 - 23:10
Session 3CSAS at Zurich D
Chair(s): Kedar Namjoshi Nokia Bell Labs
21:50
15m
Talk
Automatic Synthesis of Data-Flow AnalyzersVirtual
SAS
Xuezheng Xu UNSW Sydney, Xudong Wang UNSW Sydney, Jingling Xue UNSW Sydney
22:05
15m
Talk
Disjunctive Interval AnalysisVirtual
SAS
22:20
15m
Talk
Hash Consed Points-To SetsVirtual
SAS
Mohamad Barbar University of Technology Sydney; CSIRO’s Data61, Yulei Sui University of Technology Sydney
22:35
15m
Talk
Selective Context-Sensitivity for k-CFA with CFL-ReachabilityVirtual
SAS
Jingbo Lu UNSW Sydney, Dongjie He UNSW Sydney, Jingling Xue UNSW Sydney
22:50
20m
Live Q&A
Session 3C Discussion, Questions and Answers
SAS

Not scheduled yet

Not scheduled yet
Live Q&A
Session 2C Discussion, Questions and Answers
SAS

Not scheduled yet
Live Q&A
Session 4A Discussion, Questions and AnswersVirtual
SAS

Not scheduled yet
Live Q&A
Session 3B Discussion, Questions and Answers
SAS

Accepted Papers

Kai Jia and Martin Rinard. Exploiting Verified Neural Networks via Floating Point Numerical Error

Raphaël Monat, Abdelraouf Ouadjaout and Antoine Miné. A Multi-Language Static Analysis of Python Programs with Native C Extensions

Xuezheng Xu, Xudong Wang and Jingling Xue. Automatic Synthesis of Data-Flow Analyzer

Braine Julien, Laure Gonnord and David Monniaux. Data Abstraction: A General Framework to Handle Program Verification of Data Structures

Naoki Kobayashi, Taro Sekiyama, Issei Sato and Hiroshi Unno. Toward Neural-Network-Guided Program Synthesis and Verification

Denis Mazzucato and Caterina Urban. Reduced Products of Abstract Domains for Fairness Certification of Neural Networks

Assalé Adjé, Dorra Ben Khalifa and Matthieu Martel. Fast and Efficient Bit-Level Precision Tuning

Lucas Franceschino, David Pichardie and Jean-Pierre Talpin. Verified Functional Programming of an Abstract Interpreter

Eric Goubault, Sebastien Palumby, Sylvie Putot, Louis Rustenholz and Sriram Sankaranarayanan. Static analysis of ReLU neural networks with tropical polyhedra

Kai Jia and Martin Rinard. Verifying Low-dimensional Input Neural Networks via Input Quantization

Takumi Shimoda, Naoki Kobayashi, Ken Sakayori and Ryosuke Sato. Symbolic Automatic Relations and Their Applications to SMT and CHC Solving

Mohsen Safari, Wytse Oortwijn and Marieke Huisman. Automated Verification of the Parallel Bellman–Ford Algorithm

Scott Wesley, Maria Christakis, Arie Gurfinkel, Jorge A Navas, Richard Trefler and Valentin Wüstholz. Compositional Verification of Smart Contracts Through Communication Abstraction

David Delmas, Abdelraouf Ouadjaout and Antoine Miné. Static Analysis of Endian Portability by Abstract Interpretation

Mohamad Barbar and Yulei Sui. Hash Consed Points-To Sets

Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard and Vesal Vojdani. Improving Thread-Modular Abstract Interpretation

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sondergaard and Peter J. Stuckey. Disjunctive Interval Analysis

Yifan Chen, Chenyang Yang, Xin Zhang, Yingfei Xiong, Hao Tang, Xiaoyin Wang and Lu Zhang. Accelerating Program Analyses in Datalog by Merging Library Facts

Tianhan Lu, Bor-Yuh Evan Chang and Ashutosh Trivedi. Selectively-Amortized Resource Bounding

Jingbo Lu, Dongjie He and Jingling Xue. Selective Context-Sensitivity for k-CFA with CFL-Reachability

Divyanjali Sharma and Subodh Sharma. Thread-modular Analysis of Release-Acquire Concurrency

Marek Chalupa and Jan Strejček. Backward Symbolic Execution with Loop Folding

Call for Papers

The 28th Static Analysis Symposium, SAS 2021, will be virtually held from October 17-22, 2021 in conjunction with SPLASH. The conference may be held in a hybrid mode depending on the pandemic situation and travel restrictions.

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

  • Paper submission: April 25, 2021 — extended to April 30
  • Artifact submission: April 29, 2021 — extended to May 6
  • Author response period: June 14-18
  • Author notification: July 4
  • Final version due: August 4 (approximate)
  • Conference: Oct 17-22, 2021

Topics

The technical program for SAS 2021 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 domains
  • 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
  • Security analysis
  • Tool environments and architectures
  • Theoretical frameworks
  • Type checking

Papers

Paper submissions fall into one of two categories: regular papers and short papers.

Regular papers (18 pages max., lightweight double-blind)

Short papers (10 pages max.) may focus any of the following:

  • Experience with static analysis tools, Industrial Reports, and Case Studies (non-blind)
  • Tool papers (lightweight double-blind)
  • Brief announcements of work in progress (lightweight double-blind),
  • Well-motivated discussion of new questions or new areas (lightweight double-blind).

Papers are submitted electronically via the submission page.

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.

Papers should follow Springer’s Lecture Notes in Computer Science (LNCS) format. The page limits exclude the bibliography and well-marked appendices. Program Committee members are not required to read the appendices, thus papers must be intelligible without them.

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 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. The goal of the artifact submissions is to strengthen our field’s scientific approach to evaluations and reproducibility of results. The virtual machines will be archived on a permanent Static Analysis Symposium website to provide a record of past experiments and tools, allowing future research to better evaluate and contrast with existing work.

Artifact submission is optional. Artifact evaluation will be concurrent with paper review. More information can be found on the Call for Artifacts.

Submission Details

Lightweight Double-Blind Requirement

Other than experience reports, all other 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 papers (other than those in the first category of short 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 paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas.

Short Papers Content

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.

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.

Submission guidelines

Authors should consult Springer’s authors’ guidelines and use their proceedings templates, either for LaTeX or for Word, for the preparation of their papers. Springer encourages authors to include their ORCIDs in 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.

Camera-Ready Instructions

Below we have instructions on how to prepare and submit the camera-ready paper through EasyChair.

Deadlines (AoE)

August 18 (Wednesday):       Camera-ready version of the paper *AND* Signed copyright form

Page Limits (total number of pages)

Regular papers: 25 pages, Short papers: 15 pages.

Preparing the camera-ready version

Copyright form

We have sent the copyright form through EasyChair. Please fill in, sign, and submit along with your camera-ready version. It suffices for the corresponding author to sign the form.

Final Submission

The submission of the camera-ready version should be made on EasyChair using your “proceedings author” role for SAS 2021. Springer will require all source files and the signed copyright form. Submit (1) either a zipped file containing all your LaTeX sources or a Word file in the RTF format, and (2) the PDF version of your camera-ready paper.

Springer has an extra control loop: once data processing is finished, they will contact all corresponding authors and ask them to check their papers. We expect this to happen shortly before the printing of the proceedings. At that time your quick interaction with Springer-Verlag will be greatly appreciated.

Please feel free to reach out to us for clarifications.

Call for Artifacts

As in previous years, we encourage authors to submit any artifacts and evaluations presented in the paper. The goal of the artifact submissions is to strengthen our field’s scientific approach to evaluations and reproducibility of results. Artifact submissions also serve as a stepping stone for future research, allowing researchers to rapidly build upon existing tools, and better evaluate or contrast existing work.

Important Dates:

  • Artifact Submission: April 29, 2021 AoE May 6, 2021 AoE
  • Artifact Notification: July 4, 2021 AoE (along with the paper notification)

Criteria

This year, each artifact can be awarded up to three badges:

Validated

Artifacts which can reasonably reproduce the experimental claims in the paper. This is the minimum expectation from a submitted artifact.

Extensible

Artifacts which allow easy addition of new capabilities. To be eligible for an Extensible badge, the artifact must be bundled with the source code and pass the requirements for the Validated badge. Reviewers may attempt to tweak the source code and recompile, in order to evaluate how easy it is to build upon the tool. Please note that the artifact submission is optional. Submitting source code with the artifact is also optional. However, artifacts without source code will only be eligible for the Validated badge.

Available

Artifacts which obtain at least a Validated badge, will obtain the Available badge if the authors upload the submitted version of the artifact to the Zenodo SAS 2021 public repository. If your artifact received the Validated badge during the artifact evaluation, you can add your artifact to Zenodo SAS 2021 community by publishing your artifact here. The title and set of authors of your Zenodo submission must match with your SAS submission. The files you need to add are your artifact (virtual machine or container image) and the step-by-step instructions. After you publish your artifact, we will accept it to the community if the submission is OK, and we will award you the Available badge.

Packaging

Authors can package their artifact either as a virtual machine image or a Docker container image, and provide step-by-step instructions for loading/running the artifact.

  • Virtual machine image: The VM image must be bootable and contain all the necessary libraries installed. Please ensure that the VM image can be processed with VirtualBox. While preparing your artifact, please make it as lightweight as possible.
  • Container image: Authors can provide a zipped version of a container image containing the experiments, along with all dependencies. Please ensure that the zipped container image can be loaded using the docker load command. Please opt for container images only if your experiments can be executed and validated from the command line.
  • Step-by-step instructions: This should clearly explain how to reproduce the results that support your paper’s conclusions. We encourage the authors to include easy-to-run scripts. Note that a reviewer may be evaluating your artifact on weaker hardware compared to your setup, so try to parameterize your scripts to allow running smaller versions of your experiments. Also, you should explain how to interpret the outputs of the artifact. If possible, please provide an estimate of the execution times for the experiments. Lastly, if you are providing the source code, try to provide an outline of how the code is structured.

Submission

Please follow the instructions below to submit your artifact:

  • Package the VM/container image and the instruction document into a single compressed archive file using zip or gzip. Use your paper number for the name of the archive file.
  • Upload the archive file to well-known storage service such as Dropbox or Google Drive and get the sharable link of it.
  • Run a checksum function on the archive file. Create a text file that contains the link to the archive file and the checksum result.
  • Submit the text file via the specific submission page on EasyChair.

Badges

The SAS Artifact Evaluation badges were designed by Arpita Biswas and Suvam Mukherjee, and are available for download from GitHub.

Accepted Papers

Title
A Multi-Language Static Analysis of Python Programs with Native C ExtensionsVirtual
SAS
Pre-print Media Attached
Accelerating Program Analyses in Datalog by Merging Library FactsVirtual
SAS
Automated Verification of the Parallel Bellman--Ford AlgorithmVirtual
SAS
Automatic Synthesis of Data-Flow AnalyzersVirtual
SAS
Backward Symbolic Execution with Loop FoldingVirtual
SAS
Compositional Verification of Smart Contracts Through Communication AbstractionVirtual
SAS
Pre-print
Data Abstraction: A General Framework to Handle Program Verification of Data StructuresVirtual
SAS
Disjunctive Interval AnalysisVirtual
SAS
Exploiting Verified Neural Networks via Floating Point Numerical ErrorVirtual
SAS
Pre-print
Fast and Efficient Bit-Level Precision TuningVirtual
SAS
Hash Consed Points-To SetsVirtual
SAS
Improving Thread-Modular Abstract InterpretationVirtual
SAS
Pre-print Media Attached
Interactive Code AnalysisInvited TalkVirtual
SAS
Oracle Parfait: The Flavour of Real-World Vulnerability Detection and Intelligent ConfigurationInvited TalkVirtual
SAS
Pointer Analysis of Bytecode Programs for Effective Formal Verification of Smart ContractsInvited TalkVirtual
SAS
Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual
SAS
Selective Context-Sensitivity for k-CFA with CFL-ReachabilityVirtual
SAS
Selectively-Amortized Resource BoundingVirtual
SAS
Pre-print
Static Analysis of Endian Portability by Abstract InterpretationVirtual
SAS
Static analysis of ReLU neural networks with tropical polyhedraVirtual
SAS
Symbolic Automatic Relations and Their Applications to SMT and CHC SolvingVirtual
SAS
Thread-modular Analysis of Release-Acquire ConcurrencyVirtual
SAS
Toward Neural-Network-Guided Program Synthesis and VerificationVirtual
SAS
Verified Functional Programming of an Abstract InterpreterVirtual
SAS
Verifying Low-dimensional Input Neural Networks via Input QuantizationVirtual
SAS
Pre-print