# An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
## 3 Related Works  
In recent years, various approaches have been utilized to detect feasible paths. We point out some works in this section that are pertinent to our study. Directed automated random testing (DART) [23] was the first concolic testing study used to reduce the number of test cases to generate program paths. The paths are generated randomly based on the type of the variables, and the conditions of each path are stored until the termination of the program. However, DART suffers from a high number of duplicated paths due to the random process of generating the program paths, which leads to producing the same path more than once. Forms of early works (for example, the Concolic Unit Testing Engine (CUTE) [24] and execution generated executions (EXE) [25]) consider the system environment in the assessment by implementing external calls that make use of real and concrete arguments, which constrains the behaviors that they could delve into as compared to an entirely symbolic strategy, which could be impracticable. In the context of an online executor, this selection can lead to having external calls from distinct and well-defined paths of execution that inhibit each other. [PERSON] et al. [26] suggested a prototype PathCrawler tool for automated test case creation to meet the paths requirement. It begins with source code instrumentation in order to determine the symbolic execution sequence whenever the code being tested is executed. Figure 3: Path conditions example in symbolic execution. Subsequently, the instrumented code corresponding to the test scenario is executed until a complete feasible path set has been assessed. However, the tool faces an explosion of paths created due to extensive combinations. [PERSON] et al. [6] suggested MultiSE, where symbolic execution comprises incremental merging of the states without the use of auxiliary variables. The fundamental concept behind MultiSE is based on a different state representation, where all variables are mapped to guarded symbolic terms, referred to as a value summary. They implemented their prototype for JavaScript using the Jalangi framework [27]. However, MultiSE treats each condition separately, which increases the probability of producing duplicate paths, and it does not support web forms. [PERSON] et al. [7] illustrated the LLVM compiler-based KLEE symbolic execution software [10], which can solve optimization problems and enhance performance by an order of magnitude and process several programs that may otherwise be intractable. Its search heuristics effectively select paths from large sets of paths to obtain high code coverage. KLEE is also a crucial constituent in several ventures and research such as Cloud9 [28], GKLEE [29], KLEENet [30] and Kluver [31]. Nevertheless, the LLVM compiler is based on the algorithm formulated by [PERSON] et al. [32]. The compiler is similar to a non-SSA CFG and records the local parameters into memory, which typically are not in SSA form. The results indicated that about a quarter of the instructions created by the front end of the LLVM are in this format. [PERSON] and [PERSON] [8] suggested the Java PathFinder (JPF) translator, which translates Java to Promela, the modeling language required for using the Spin model checker. JPF transforms specified Java code to its corresponding Promela version, which may then be processed. The key drawback of this tool is that it cannot be utilized for substantiating any authentic Java application if no non-trivial quantity of work is completed by its user. For the resolution of this issue, [PERSON] and [PERSON] [33] recommended an extension, jpf-nhandler, of JPF that enables automation of the handling of native methodologies. Automation of the interlinking for the execution of the native code and the model checking of Java code occurs. However, the extension lacks soundness and, as the author of [33] stated, it is not comprehensive. [PERSON] et al. [34] proposed a method (CFT4 CUnit) for creating static direction-based test cases specific to C functions.