Symbolic state validation through runtime data

Abstract

Real world programs are typically built on top of many library functions. Symbolic analysis of these programs generally requires precise models of these functions? Application Programming Interfaces (APIs), which are mostly unavailable because these models are costly to construct. A variant approach of symbolic analysis is to over-approximate the return values of those APIs that have not been modeled. However, such approximation can induce many unreachable symbolic states, which are expensive to validate manually. In this paper, we propose a static approach to automatically validating the reported anomalous symbolic states. The validation makes use of the available runtime data of the un-modeled APIs collected from previous program executions. We show that the symbolic state validation problem can be cast as a MAX-SAT problem and solved by existing constraint solvers.