Sun 20 Oct 2024 11:30 - 12:00 at San Gabriel - Types, Control-flow and trace partitioning Chair(s): Michele Pasqua

Static analyzers can exhibit a variety of control-flow sensitivities, including path and flow sensitivity. Darais et al. provide an account of these sensitivities rooted in “control properties of the interpreter” for static analyzers that model program behavior as a finite-state transition system. In the meantime, many static analyzer frameworks—particularly those for higher-order languages—have migrated to more sophisticated and precise pushdown models which admit evaluation summaries. It is not immediately clear how to realize the full spectrum of path and flow sensitivity in a summary-based setting which, like that of Darais et al., is rooted in the control properties of the interpreter and therefore independent of all other aspects of the analyzer formulation. We present a framework which achieves precisely this. We also provide a caching algorithm which performs summarization and demonstrate the framework on an abstract definitional interpreter. Altogether, we show how to achieve the full range of path and flow sensitivities, even at once, within a single abstract definitional interpreter-based analysis, completely independent of other aspects of its formulation.

Sun 20 Oct

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

11:00 - 12:30
Types, Control-flow and trace partitioningSAS at San Gabriel
Chair(s): Michele Pasqua University of Verona
11:00
30m
Full-paper
BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code
SAS
Ian Smith Trail of Bits
Pre-print
11:30
30m
Full-paper
Full Control-Flow Sensitivity for Definitional Interpreters
SAS
Kimball Germane Brigham Young University
Pre-print
12:00
30m
Full-paper
Trace Partitioning as an Optimization Problem
SAS
Charles Babu M CEA-List, Matthieu Lemerre Université Paris-Saclay - CEA LIST, Sébastien Bardin CEA LIST, University Paris-Saclay, Jean-Yves Marion LORIA
Pre-print