IEEE/ICACT20260382 Slide.10        [Big Slide]       Oral Presentation
Here is how our algorithm works. We start symbolic execution at the beginning of the path, treating the initial function arguments as symbolic variables. To stay focused, we prune any branches that lead outside our target path, preventing unnecessary execution. If the execution reaches the endpoint and verifies that every required block was executed, it reports the path as feasible. However, if the execution finishes without reaching the endpoint—or if blocks are skipped—we know the path is infeasible.

[Go to Next Slide]
Select Voice: