摘要：interpretation is a static analysis framework for sound over-approximation of all possible runtime states of a program. Symbolic execution is a framework for reachability analysis which tries to explore all possible execution paths of a program. A shared feature between interpretation and symbolic execution is that each - implicitly or explicitly - maintains constraints during execution, in the form of invariants or path conditions. We investigate the relations between the worlds of interpretation, symbolic execution and constraint solving, to expose potential synergies.
