When to Stop Going Down the Rabbit Hole: Taming Context-Sensitivity on the Fly
Context-sensitive analysis of programs containing recursive procedures may be expensive, in particular, when using expressive domains, rendering the set of possible contexts large or even infinite. Here, we present a general framework for context-sensitivity that allows formalizing not only known approaches such as full-context or call strings but also combinations of these. We propose three generic lifters in this framework to bound the number of encountered contexts on the fly. These lifters are implemented within the abstract interpreter Goblint and compared to existing approaches to context-sensitivity on the SV-COMP benchmark suite. On a subset of recursive benchmarks, all proposed lifters manage to reduce the number of stack-overflows and timeouts compared to a full context approach, with one of them improving the number of correct verdicts by 31% and showing promising results on the considered SV-COMP categories.
Tue 25 JunDisplayed time zone: Windhoek change
13:40 - 15:20 | |||
13:40 50mKeynote | Lightweight Resource Leak Verification and Inference SOAP Manu Sridharan University of California at Riverside | ||
14:30 20mTalk | Interactive Source-to-Source Optimizations Validated using Static Resource Analysis SOAP Guillaume Bertholon Inria & Université de Strasbourg, CNRS, ICube, France, Arthur Charguéraud Inria; Université de Strasbourg; CNRS; ICube, Thomas Koehler INRIA, Begatim Bytyqi Inria & Université de Strasbourg, CNRS, ICube, France, Damien Rouhling Inria Nancy Grand-Est; France | ||
14:50 20mTalk | When to Stop Going Down the Rabbit Hole: Taming Context-Sensitivity on the Fly SOAP Julian Erhard Technical University of Munich, Johanna Franziska Schinabeck Technische Universität München, Michael Schwarz Technische Universität München, Helmut Seidl Technische Universität München |