Efficient loop navigation for symbolic execution

DOI10.1007/978-3-642-24372-1_34zbMATH Open1348.68146arXiv1107.1398OpenAlexW1507201375MaRDI QIDQ3172934FDOQ3172934

Jan Obdržálek, Marek Trtík

Publication date: 7 October 2011

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Abstract: Symbolic execution is a successful and very popular technique used in software verification and testing. A key limitation of symbolic execution is in dealing with code containing loops. The problem is that even a single loop can generate a huge number of different symbolic execution paths, corresponding to different number of loop iterations and taking various paths through the loop. We introduce a technique which, given a start location above some loops and a target location anywhere below these loops, returns a feasible path between these two locations, if such a path exists. The technique infers a collection of constraint systems from the program and uses them to steer the symbolic execution towards the target. On reaching a loop it iteratively solves the appropriate constraint system to find out which path through this loop to take, or, alternatively, whether to continue below the loop. To construct the constraint systems we express the values of variables modified in a loop as functions of the number of times a given path through the loop was executed. We have built a prototype implementation of our technique and compared it to state-of-the-art symbolic execution tools on simple programs with loops. The results show significant improvements in the running time. We found instances where our algorithm finished in seconds, whereas the other tools did not finish within an hour. Our approach also shows very good results in the case when the target location is not reachable by any feasible path.

Full work available at URL: https://arxiv.org/abs/1107.1398

Recommendations

• Loop invariant symbolic execution for parallel programs
• Symbolic execution: A semantic approach
• Symbolic execution as DPLL modulo theories
• Model Checking Software
• Backward symbolic execution with loop folding

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (4)

• Symbolic execution: A semantic approach
• Symbolic Loop Bound Computation for WCET Analysis
• Embedded software verification using symbolic execution and uninterpreted functions
• Tools and Algorithms for the Construction and Analysis of Systems

Uses Software

• CUTE
• KLEE
• DART
• Pex
• YOGI

This page was built for publication: Efficient loop navigation for symbolic execution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172934)