SAS 2020
Wed 18 - Fri 20 November 2020 Online Conference
co-located with SPLASH 2020
Wed 18 Nov 2020 15:00 - 15:20 at SPLASH-III - 4 Chair(s): Antoine Miné, Jeremy G. Siek
Thu 19 Nov 2020 03:00 - 03:20 at SPLASH-III - 4 Chair(s): Shigeru Chiba, Caterina Urban

Practical adoption of static analysis often requires trading precision for performance. This paper focuses on improving the memory efficiency of abstract interpretation without sacrificing precision or time efficiency. Computationally, abstract interpretation reduces the problem of inferring program invariants to computing a fixpoint of a set of equations. This paper presents a method to minimize the memory footprint in Bourdoncle’s iteration strategy, a widely-used technique for fixpoint computation. Our technique is agnostic to the abstract domain used. We prove that our technique is optimal (i.e., it results in minimum memory footprint) for Bourdoncle’s iteration strategy while computing the same result. We evaluate the efficacy of our technique by implementing it in a tool called MIKOS, which extends the state-of-the-art abstract interpreter IKOS. When verifying user-provided assertions, MIKOS shows a decrease in peak-memory usage to 4.07% (24.57x) on average compared to IKOS. When performing interprocedural buffer-overflow analysis, MIKOS shows a decrease in peak-memory usage to 43.7% (2.29x) on average compared to IKOS.

Wed 18 Nov

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

15:00 - 16:20
4DLS / SAS at SPLASH-III +12h
Chair(s): Antoine Miné Sorbonne Université, Jeremy G. Siek Indiana University, USA
15:00
20m
Research paper
Memory-Efficient Fixpoint ComputationArtifact
SAS
Sung Kook Kim University of California, Davis, Arnaud J. Venet Facebook, Aditya V. Thakur University of California, Davis
Pre-print Media Attached
15:20
20m
Talk
Dynamic Pattern Matching with Python
DLS
Tobias Kohn University of Cambridge, UK, Guido van Rossum Python Software Foundation, Brandt Bucher Research Affiliates, LLC, Talin , Ivan Levkivskyi Dropbox Ireland
Link to publication DOI Media Attached
15:40
20m
Research paper
Simple and Efficient Computation of Minimal Weak Control ClosureArtifact
SAS
Abu Naser Masud Malardalen University
Media Attached File Attached
16:00
20m
Talk
Sound, Heuristic Type Annotation Inference for Ruby
DLS
Milod Kazerounian University of Maryland, College Park, Brianna M. Ren University of Maryland, Jeffrey S. Foster Tufts University
Link to publication DOI Pre-print Media Attached

Thu 19 Nov

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

03:00 - 04:20
4SAS / DLS at SPLASH-III
Chair(s): Shigeru Chiba The University of Tokyo, Caterina Urban École normale supérieure
03:00
20m
Research paper
Memory-Efficient Fixpoint ComputationArtifact
SAS
Sung Kook Kim University of California, Davis, Arnaud J. Venet Facebook, Aditya V. Thakur University of California, Davis
Pre-print Media Attached
03:20
20m
Talk
Dynamic Pattern Matching with Python
DLS
Tobias Kohn University of Cambridge, UK, Guido van Rossum Python Software Foundation, Brandt Bucher Research Affiliates, LLC, Talin , Ivan Levkivskyi Dropbox Ireland
Link to publication DOI Media Attached
03:40
20m
Research paper
Simple and Efficient Computation of Minimal Weak Control ClosureArtifact
SAS
Abu Naser Masud Malardalen University
Media Attached File Attached
04:00
20m
Talk
Sound, Heuristic Type Annotation Inference for Ruby
DLS
Milod Kazerounian University of Maryland, College Park, Brianna M. Ren University of Maryland, Jeffrey S. Foster Tufts University
Link to publication DOI Pre-print Media Attached