TY - GEN
T1 - PREACH
T2 - 44th ACM/IEEE International Conference on Software Engineering, ICSE 2022
AU - Saha, Seemanta
AU - Downing, Mara
AU - Brennan, Tegan
AU - Bultan, Tevfik
N1 - Publisher Copyright:
© 2022 ACM.
PY - 2022
Y1 - 2022
N2 - We present a heuristic for approximating the likelihood of reaching a given program statement using 1) branch selectivity (representing the percentage of values that satisfy a branch condition), which we compute using model counting, 2) dependency analysis, which we use to identify input-dependent branch conditions that influence statement reachability, 3) abstract interpretation, which we use to identify the set of values that reach a branch condition, and 4) a discrete-time Markov chain model, which we construct to capture the control flow structure of the program together with the selectivity of each branch. Our experiments indicate that our heuristic-based probabilistic reachability analysis tool PReach can identify hard to reach statements with high precision and accuracy in benchmarks from software verification and testing competitions, Apache Commons Lang, and the DARPA STAC program. We provide a detailed comparison with probabilistic symbolic execution and statistical symbolic execution for the purpose of identifying hard to reach statements. PREACH achieves comparable precision and accuracy to both probabilistic and statistical symbolic execution for bounded execution depth and better precision and accuracy when execution depth is unbounded and the number of program paths grows exponentially. Moreover, PReach is more scalable than both probabilistic and statistical symbolic execution.
AB - We present a heuristic for approximating the likelihood of reaching a given program statement using 1) branch selectivity (representing the percentage of values that satisfy a branch condition), which we compute using model counting, 2) dependency analysis, which we use to identify input-dependent branch conditions that influence statement reachability, 3) abstract interpretation, which we use to identify the set of values that reach a branch condition, and 4) a discrete-time Markov chain model, which we construct to capture the control flow structure of the program together with the selectivity of each branch. Our experiments indicate that our heuristic-based probabilistic reachability analysis tool PReach can identify hard to reach statements with high precision and accuracy in benchmarks from software verification and testing competitions, Apache Commons Lang, and the DARPA STAC program. We provide a detailed comparison with probabilistic symbolic execution and statistical symbolic execution for the purpose of identifying hard to reach statements. PREACH achieves comparable precision and accuracy to both probabilistic and statistical symbolic execution for bounded execution depth and better precision and accuracy when execution depth is unbounded and the number of program paths grows exponentially. Moreover, PReach is more scalable than both probabilistic and statistical symbolic execution.
UR - http://www.scopus.com/inward/record.url?scp=85133552605&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85133552605&partnerID=8YFLogxK
U2 - 10.1145/3510003.3510227
DO - 10.1145/3510003.3510227
M3 - Conference contribution
AN - SCOPUS:85133552605
T3 - Proceedings - International Conference on Software Engineering
SP - 1706
EP - 1717
BT - Proceedings - 2022 ACM/IEEE 44th International Conference on Software Engineering, ICSE 2022
Y2 - 22 May 2022 through 27 May 2022
ER -