# An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
## 4 Detection Methodology
### Avoid Duplicated Feasible Paths
\begin{tabular}{l l} \(B\) & Program branches \\ \(CB\) & The total number of Conditional Blocks in the current path \\ \(CBV\) & List of the current block variables \\ \(\mathbf{DF}_{Detected}\) & The number of duplicated feasible paths detected \\ \(\mathbf{F}_{True}\) & The number of feasible paths that exist in the detected program \\ \(\mathbf{F}_{False}\) & The number of feasible paths detected that are infeasible in reality \\ \(F_{Detected}\) & The number of feasible paths detected \\ \(GP\) & List of all generated paths \\ \(i\) & Instructions \\ \(LO\) & The total number of Logical Operators in the path \\ \end{tabular} 

## Appendix A

This section shows samples of the results of the proposed approach on the Peruggia 1.1 application. ### Appendix A.1

Figure 11 shows a feasible path that was correctly detected as a feasible path (not duplicated). The first part shows the symbolic variables of this path, followed by the conditions that were extracted from this path. The green font color shows the Z3 solver results with a value for each symbolic variable that Z3 solver suggests satisfies this condition. The last two lines show the path weight value (7.75) and the type of path (a new path that is not duplicated). ### Appendix A.2

Figure 11 shows a duplicated feasible path that was detected as a duplicated path. The first section shows the symbolic variables of this path. followed by the conditions that were extracted from this path. Since the path weight was similar to a path that was detected previously (7.24), this path was considered as duplicated, and it did not pass to the next step (the feasibility check). The last line shows the path results for duplicated paths. ## Appendix A

Figure 14 shows the final results of analyzing the Peruggia application, where 3664 instructions (I) and 59 branches (B) were analyzed. A total number of 235 feasible paths (FPD) was detected, while 462 duplicated feasible paths (DFP) were avoided within 1.862 s.

## References

* [PERSON] and [PERSON] (2020) [PERSON]; [PERSON] [PERSON] A Review on Benchmarking: Comparing the Static Analysis Tools (SATs) in Web Security. In _Social Networking and Computational Intelligence_; Springer: Berlin/Heidelberg, Germany, 2020; pp. 327-337. [CrossRef]
* [PERSON] et al. (2019) [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] sCompile: Critical path identification and analysis for smart contracts. In _International Conference on Formal Engineering Methods_; Springer: Berlin/Heidelberg, Germany, 2019; pp. 286-304. [CrossRef]
* [PERSON] and [PERSON] (2018) [PERSON]; [PERSON]; [PERSON] The Problems and Challenges of Infeasible Paths in Static Analysis. _Int. J. Eng. Technol._**2018**, \(7\), 412-417. * [PERSON] et al. (2019) [PERSON]; [PERSON]; [PERSON] Multi-objective multi-robot path planning in continuous environment using an enhanced genetic algorithm. _Expert Syst. Appl._**2019**, _115_, 106-120. [CrossRef]
* [PERSON] (2020) [PERSON] [PERSON] Automatic support for the identification of infeasible testing requirements. In Proceedings of the 29 th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, 18-22 July 2020; pp. 587-591. [CrossRef]
* [PERSON] et al. (2015) [PERSON]; [PERSON]; [PERSON]; [PERSON] MultiSE: Multi-path symbolic execution using value summaries. In Proceedings of the 2015 10 th Joint Meeting on Foundations of Software Engineering, Bergamo, Italy, 30 August-4 September 2015; pp. 842-853. [CrossRef][PERSON]; [PERSON]; [PERSON]: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8 th USENIX Symposium on Operating Systems Design and Implementation (OSDI '08), San Diego, CA, USA, 8-10 December 2008; pp. 209-224. * [PERSON] and [PERSON] (2000) [PERSON]; [PERSON] Model checking java programs using java pathfinder. _Int. J. Softw. Tools Technol. Transf._**2000**, \(2\), 366-381. [CrossRef]
* [PERSON] et al. (2015) [PERSON]; [PERSON]; [PERSON] [PERSON] A graph-based higher-order intermediate representation.