Mon 5 DecDisplayed 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 60mKeynote | Commercial-Grade Static Analyzers in DatalogIn PersonKeynote SAS Bernhard Scholz University of Sydney |
10:30 - 12:00 | |||
10:30 30mTalk | 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 30mTalk | 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 30mTalk | Case Study on Verification-Witness Validators: Where We Are and Where We Go SAS Link to publication DOI Media Attached |
13:30 - 15:00 | Numerical Static AnalysesSAS at AMRF Auditorium Chair(s): Isabella Mastroeni University of Verona, Italy | ||
13:30 30mTalk | 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 30mTalk | Boosting Robustness Verification of Semantic Feature Neighborhoods SAS | ||
14:30 30mTalk | 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: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 60mKeynote | Logical Reasoning in Reinforcement Learning: A Boon or Bane? KeynoteVirtual SAS Suguman Bansal Rice University, USA | ||
16:30 10mAwards | Radhia Cousot Award SAS Caterina Urban Inria & École Normale Supérieure | Université PSL, Gagandeep Singh University of Illinois at Urbana-Champaign | ||
16:40 20mDay closing | PC Chairs Report SAS Caterina Urban Inria & École Normale Supérieure | Université PSL, Gagandeep Singh University of Illinois at Urbana-Champaign |
Tue 6 DecDisplayed 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 60mKeynote | Towards Efficient Reasoning of Quantum ProgramsKeynote SAS Nengkun Yu Stony Brook University, USA |
10:30 - 12:00 | |||
10:30 30mTalk | 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 30mTalk | Adversarial Logic SAS Julien Vanegue Bloomberg | ||
11:30 30mTalk | Property-driven code obfuscations - Reinterpreting Jones-optimality in Abstract Interpretation SAS |
13:30 - 15:00 | |||
13:30 30mTalk | Invariant Inference With Provable Complexity From the Monotone Theory SAS | ||
14:00 30mTalk | 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 30mTalk | 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:30 - 17:00 | |||
15:30 30mTalk | Bootstrapping Library-Based Synthesis SAS | ||
16:00 30mTalk | 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 30mTalk | Solving Invariant Generation for Unsolvable Loops SAS Daneshvar Amrollahi Stanford University, Ezio Bartocci TU Wien, George Kenison TU Wien, Laura Kovács TU Wien, Marcel Moosbrugger TU Wien, Miroslav Stankovič TU Wien |
Wed 7 DecDisplayed time zone: Auckland, Wellington change
10:30 - 12:00 | |||
10:30 30mTalk | 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 30mTalk | Principles of Staged Static+Dynamic Partial Analysis SAS | ||
11:30 30mTalk | Fast and incremental computation of weak control closure SAS Abu Naser Masud Malardalen University |
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: May 18, 2022 AoE
Are you running late in preparing your artifact? No worries! Deadline is extended to the 25th!
- Artifact Notification: July 15, 2022 AoE (along with the paper notification)
Criteria
This year, as last 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 2022 public repository. If your artifact received the Validated badge during the artifact evaluation, you can add your artifact to Zenodo SAS 2022 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. Consider installing
ssh
in the VM to make it reachable even when virtual screen isn’t working (common problem when changing host hardware). - 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.