Formalizing Symbolic Execution Path Explosion for Recursive Functions via Asymptotic Path Complexity
Path coverage is of critical importance in software testing and verification. Further, path explosion is a well-known challenge for automatic software analysis techniques like symbolic execution. Asymptotic Path Complexity (APC) is a code complexity metric that formalizes the quantitative measurement of path explosion and therefore measures the difficulty of achieving path coverage. Prior methods were unable to correctly compute APC for recursive functions as the methods used were not sufficiently expressive to model the path explosion behavior in recursive functions (existing analyses simply ignored recursive calls). We present a novel method for computing asymptotic path complexity for recursive functions, which we call APC-R. Our approach is based on the analytic combinatorics of context free grammars. We implemented our approach on top of the code complexity analysis tool Metrinome and evaluated our implementation on a set of benchmark programs written in the C programming language. Our experiments demonstrate that APC-R is a sound upper bound on the growth rate of the number of program paths explored for increasing exploration depth when generating tests with the KLEE symbolic execution engine. Our APC-R implementation provides sound bounds on KLEE’s symbolic execution path explosion for recursive functions in cases where the original APC implementation did not, and APC-R matches the results of APC for non-recursive functions with only marginal computational overhead. That is, our more expressive APC-R subsumes earlier APC work without significant performance cost.
Sun 14 MayDisplayed time zone: Hobart change
15:45 - 17:15 | |||
15:45 30mPaper | Mutant Equivalence as Monotonicity in Parametric Timed Games FormaliSE 2023 Davide Basile Formal Methods and Tools lab, ISTI-CNR, Pisa, Italy, Maurice ter Beek ISTI-CNR, Pisa, Italy, Hendrik Göttmann Technical University of Darmstadt, Malte Lochau University of Siegen | ||
16:15 30mPaper | Differential Testing of a Verification Framework for Compiler Optimizations (Case Study) FormaliSE 2023 Mark Utting The University of Queensland, Brae J. Webb The University of Queensland, Ian J. Hayes The University of Queensland | ||
16:45 30mPaper | Formalizing Symbolic Execution Path Explosion for Recursive Functions via Asymptotic Path Complexity FormaliSE 2023 Eli Pregerson Harvey Mudd College, Shaheen Cullen-Baratloo Harvey Mudd College, David Chen Harvey Mudd College, Duy Lam Harvey Mudd College, Max Szostak Harvey Mudd College, Lucas Bang Harvey Mudd College |