FormaliSE 2023
Dates to be announced Melbourne, Australia
co-located with ICSE 2023
Sun 14 May 2023 16:45 - 17:15 at Meeting Room 102 - Testing Chair(s): Cristian Cadar

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 May

Displayed time zone: Hobart change

15:45 - 17:15
TestingFormaliSE 2023 at Meeting Room 102
Chair(s): Cristian Cadar Imperial College London, UK
15:45
30m
Paper
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
30m
Paper
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
30m
Paper
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