SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
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, Simmo 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, Simmo 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 École normale supérieure
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 New South Wales, 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 École normale supérieure
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 New South Wales, 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