Program Path Feasibility Through Symbolic Execution

This article introduces a method for checking program control flow path feasibility through symbolic execution.We present an automatic symbolization approaches that target these important parts: variables with unknown values, function arguments and return values, and pointerreferenced memories.The proposed techniques make symbolic execution more practical for software testing and verification.We also introduce an algorithm for program control flow path verification that utilizes the mentioned enhancements.As the symbolic execution is a resource-demanding process, the path verification algorithm eliminates redundant program branches.This feature is integrated into a static analysis tool for more accurate analysis.