Minimizing the Size of Path Conditions Using Convex Polyhedra Abstract Domain

Symbolic execution (SE) is a path-sensitive program analysis technique widely used in program verification. As it interprets a program path on symbolic inputs, SE generates a set of constraints called a path condition (PC). A PC describes possible concrete values that can traverse the same path during program execution. In order to determine whether such a set is non-empty, symbolic execution utilizes constraint solvers to determine whether a PC is satisfiable. The further SE explores a program path, the more constraints are added to PCs. This raises the issue of the scalability of the approach since SE needs more memory to store large PCs and a solver needs additional time to decide them. Approaches such as,slicing and decomposition of a PC addresses the latter but not the former issue. In this work we propose an orthogonal to the previous efforts technique that minimizes the number of constraints in a PC. The idea is to identify in the PC a set of linear constraints describing a polyhedron and use effiocient techniques to remove the redundant constraints in that set. In this work, we outsource this task to Parma Polyhedra Library (PPL). Our experiments have shown that this approach reduced the size of PCs and if a solver is insensitive to the PPL\u27s constraint format the solver\u27s time to decide PCs is reduced also