TY - GEN
T1 - When to Stop Going Down the Rabbit Hole
T2 - 13th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, SOAP 2024, co-located with the 45th ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2024
AU - Erhard, Julian
AU - Schinabeck, Johanna Franziska
AU - Schwarz, Michael
AU - Seidl, Helmut
N1 - Publisher Copyright:
Copyright © 2024 is held by the owner/author(s). Publication rights licensed to ACM.
PY - 2024/6/20
Y1 - 2024/6/20
N2 - 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.
AB - 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.
KW - abstract interpretation
KW - context-sensitive analysis
KW - software verification
KW - static program analysis
UR - https://www.scopus.com/pages/publications/85198642046
U2 - 10.1145/3652588.3663321
DO - 10.1145/3652588.3663321
M3 - Conference contribution
AN - SCOPUS:85198642046
T3 - SOAP 2024 - Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, Co-located with: PLDI 2024
SP - 35
EP - 44
BT - SOAP 2024 - Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, Co-located with
PB - Association for Computing Machinery, Inc
Y2 - 25 June 2024
ER -