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

Imprecision is a very common phenomenon in static analyses that results in false alarms when used for program verification. Designing automatic techniques to improve static analysis precision is an old dream, but it is highly non-trivial. In the last two decades, static analysis gave rise to refinement techniques to improve precision through various forms of sensitivity. Yet, prior attempts are either specialized to particular domains or based on syntactic rules and heuristics that are tedious to design and prone to path explosion. In this paper, we cast the problem of improving static analysis precision as an optimization problem and propose a generic search-based method to solve it. We identify the challenges that one faces when solving this problem (like the large search space, path explosion, redundant computations, or non-monotonic operations in abstract domains) and provide adequate solutions to each. Finally, we provide a first implementation of the method, demonstrating both its feasibility and potential over standard benchmark (our early pro- totype is able to prove some goals that state-of-the-art software model checkers cannot), and providing valuable feedback when implementing this method in a static analyzer.

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