SAS 2022
Mon 5 - Wed 7 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Dates
Tracks
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: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
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: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: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: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 Lahiri Microsoft Research
16:30
30m
Talk
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 Dec

Displayed time zone: Auckland, Wellington change

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

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.

Questions? Use the SAS Artifacts contact form.