An Approach to Static-Dynamic Software Analysis

Abstract. Safety-critical software in industry is typically subjected to both dy-namic testing as well as static program analysis. However, while testing is ex-pensive to scale, static analysis is prone to false positives and/or false nega-tives. In this work we propose a solution based on a combination of static anal-ysis to zoom into potential bug candidates in large code bases and symbolic execution to confirm these bugs and create concrete witnesses. Our proposed approach is intended to maintain scalability while improving precision and as such remedy the short comings of each individual solution. Moreover, we de-veloped the SEEKFAULT tool that creates local symbolic execution targets from static analysis bug candidates and evaluate its effectiveness on the SV-COMP loop benchmarks. We show that a conservative tuning can achieve a 98 % de-tecting rate in that benchmark while at the same time reducing false positive rates by around 50 % compared to a singular static analysis approach.