Enhancing Symbolic Execution with Built-In Term Rewriting and Constrained Lazy Initialization

Symbolic execution su ffers from problems when analyzing programs that handle complex data structures as their inputs and take decisions over non-linear expressions. For these programs, symbolic execution may incur invalid inputs or unidentifi ed infeasible traces, and may raise large amounts of false alarms. Some symbolic executors tackle these problems by introducing executable preconditions to exclude invalid inputs, and some solvers exploit rewrite rules to address non linear problems. In this paper, we discuss the core limitations of executable preconditions, and address these limitations by proposing invariants speci fically designed to harmonize with the lazy initialization algorithm. We extend the scope of applicability of term rewriting by a set of rewrite rules applied within the symbolic executor, to address simpli cations of inverse relationships fostered from either program-specifi c calculations or the logic of the veri fication tasks. We present a symbolic executor that integrates the two techniques, and validate our approach against the veri cation of a relevant set of properties of the Tactical Separation Assisted Flight Environment (TSAFE). The empirical data show that the integrated approach can improve the eff ectiveness of symbolic execution