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 OctDisplayed 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 30mFull-paper | BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code SAS Ian Smith Trail of Bits Pre-print | ||
11:30 30mFull-paper | Full Control-Flow Sensitivity for Definitional Interpreters SAS Kimball Germane Brigham Young University Pre-print | ||
12:00 30mFull-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 |