PLDI 2024
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark
Tue 25 Jun 2024 14:50 - 15:10 at Reykjavik - SOAP III Chair(s): Cindy Rubio-González

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 Jun

Displayed time zone: Windhoek change

13:40 - 15:20
SOAP IIISOAP at Reykjavik
Chair(s): Cindy Rubio-González University of California at Davis
13:40
50m
Keynote
Lightweight Resource Leak Verification and Inference
SOAP
Manu Sridharan University of California at Riverside
14:30
20m
Talk
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
20m
Talk
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