Parallel Program Analysis on Path Ranges
CoRR(2024)
摘要
Symbolic execution is a software verification technique symbolically running
programs and thereby checking for bugs. Ranged symbolic execution performs
symbolic execution on program parts, so called path ranges, in parallel. Due to
the parallelism, verification is accelerated and hence scales to larger
programs.
In this paper, we discuss a generalization of ranged symbolic execution to
arbitrary program analyses. More specifically, we present a verification
approach that splits programs into path ranges and then runs arbitrary analyses
on the ranges in parallel. Our approach in particular allows to run different
analyses on different program parts. We have implemented this generalization on
top of the tool CPAchecker and evaluated it on programs from the SV-COMP
benchmark. Our evaluation shows that verification can benefit from the
parallelisation of the verification task, but also needs a form of work
stealing (between analyses) as to become efficient
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要