SPLASH 2021 (series) / SAS 2021 (series) /
SAS 2021 Program
This is the SAS 2021 program - see the full program for SPLASH 2021 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 17 OctDisplayed time zone: Central Time (US & Canada) change
Sun 17 Oct
Displayed time zone: Central Time (US & Canada) change
09:00 - 10:20 | |||
09:00 15mTalk | 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 15mTalk | Exploiting Verified Neural Networks via Floating Point Numerical ErrorVirtual SAS Pre-print | ||
09:30 15mTalk | 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 15mTalk | 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 20mLive Q&A | Session 1A Discussion, Questions and Answers Virtual SAS | ||
13:50 - 15:10 | |||
13:50 15mTalk | Static Analysis of Endian Portability by Abstract InterpretationVirtual SAS David Delmas Airbus & Sorbonne Université, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université | ||
14:05 15mTalk | Verified Functional Programming of an Abstract InterpreterVirtual SAS | ||
14:30 15mTalk | Data Abstraction: A General Framework to Handle Program Verification of Data StructuresVirtual SAS | ||
14:45 25mLive Q&A | Session 3A Discussion, Questions and AnswersVirtual SAS | ||
15:40 - 17:00 | |||
15:40 80mKeynote | Oracle Parfait: The Flavour of Real-World Vulnerability Detection and Intelligent ConfigurationInvited TalkVirtual SAS Cristina Cifuentes Oracle Labs | ||
17:00 - 18:20 | |||
17:00 15mTalk | 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 15mTalk | Exploiting Verified Neural Networks via Floating Point Numerical ErrorVirtual SAS Pre-print | ||
17:30 15mTalk | 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 15mTalk | 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 20mLive Q&A | Session 1A Discussion, Questions and Answers Virtual SAS | ||
21:50 - 23:10 | |||
21:50 15mTalk | Static Analysis of Endian Portability by Abstract InterpretationVirtual SAS David Delmas Airbus & Sorbonne Université, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université | ||
22:05 15mTalk | Verified Functional Programming of an Abstract InterpreterVirtual SAS | ||
22:30 15mTalk | Data Abstraction: A General Framework to Handle Program Verification of Data StructuresVirtual SAS | ||
22:45 25mLive Q&A | Session 3A Discussion, Questions and AnswersVirtual SAS | ||
Mon 18 OctDisplayed time zone: Central Time (US & Canada) change
Mon 18 Oct
Displayed time zone: Central Time (US & Canada) change
07:40 - 09:00 | |||
07:40 15mTalk | 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 15mTalk | Backward Symbolic Execution with Loop FoldingVirtual SAS | ||
08:10 15mTalk | 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 15mTalk | 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 20mLive Q&A | Session 4B Discussion, Questions and Answers SAS | ||
10:50 - 12:10 | |||
10:50 15mTalk | 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 15mTalk | 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 15mTalk | Thread-modular Analysis of Release-Acquire ConcurrencyVirtual SAS | ||
11:35 35mLive Q&A | Session 2B Discussion, Questions and Answers SAS | ||
13:50 - 15:10 | |||
13:50 80mKeynote | Interactive Code AnalysisInvited TalkVirtual SAS | ||
15:40 - 17:00 | |||
15:40 15mTalk | 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 15mTalk | Backward Symbolic Execution with Loop FoldingVirtual SAS | ||
16:10 15mTalk | 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 15mTalk | 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 20mLive Q&A | Session 4B Discussion, Questions and Answers SAS | ||
18:50 - 20:10 | |||
18:50 15mTalk | 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 15mTalk | 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 15mTalk | Thread-modular Analysis of Release-Acquire ConcurrencyVirtual SAS | ||
19:35 35mLive Q&A | Session 2B Discussion, Questions and Answers SAS | ||
Tue 19 OctDisplayed time zone: Central Time (US & Canada) change
Tue 19 Oct
Displayed time zone: Central Time (US & Canada) change
07:40 - 09:00 | |||
07:40 15mTalk | 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 15mTalk | Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual SAS | ||
08:10 15mTalk | 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 15mTalk | 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 20mLive Q&A | Session 4C Discussion, Questions and AnswersVirtual SAS | ||
10:50 - 12:10 | |||
10:50 80mTalk | Pointer Analysis of Bytecode Programs for Effective Formal Verification of Smart ContractsInvited TalkVirtual SAS Mooly Sagiv Tel Aviv University | ||
13:50 - 15:10 | |||
13:50 15mTalk | Automatic Synthesis of Data-Flow AnalyzersVirtual SAS | ||
14:05 15mTalk | Disjunctive Interval AnalysisVirtual SAS Graeme Gange , Jorge A. Navas SRI International, Peter Schachte , Harald Sondergaard , Peter J. Stuckey Monash University | ||
14:20 15mTalk | 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 15mTalk | Selective Context-Sensitivity for k-CFA with CFL-ReachabilityVirtual SAS | ||
14:50 20mLive Q&A | Session 3C Discussion, Questions and Answers SAS | ||
15:40 - 17:00 | |||
15:40 15mTalk | 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 15mTalk | Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual SAS | ||
16:10 15mTalk | 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 15mTalk | 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 20mLive Q&A | Session 4C Discussion, Questions and AnswersVirtual SAS | ||
21:50 - 23:10 | |||
21:50 15mTalk | Automatic Synthesis of Data-Flow AnalyzersVirtual SAS | ||
22:05 15mTalk | Disjunctive Interval AnalysisVirtual SAS Graeme Gange , Jorge A. Navas SRI International, Peter Schachte , Harald Sondergaard , Peter J. Stuckey Monash University | ||
22:20 15mTalk | 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 15mTalk | Selective Context-Sensitivity for k-CFA with CFL-ReachabilityVirtual SAS | ||
22:50 20mLive Q&A | Session 3C Discussion, Questions and Answers SAS | ||