Empc: Effective Path Prioritization for Symbolic Execution with Path Cover

• URL: http://arxiv.org/abs/2505.03555v1
• Date: Tue, 06 May 2025 14:08:36 GMT
• Title: Empc: Effective Path Prioritization for Symbolic Execution with Path Cover
• Authors: Shuangjie Yao, Dongdong She,
• Abstract summary: Symbolic execution can formally reason the correctness of program behaviors and detect software bugs.<n>It suffers from an inherent limitation: path explosion.<n>We propose a novel and effective path prioritization technique with path cover, named Empc.
• Score: 4.247960711260534
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic execution is a powerful program analysis technique that can formally reason the correctness of program behaviors and detect software bugs. It can systematically explore the execution paths of the tested program. But it suffers from an inherent limitation: path explosion. Path explosion occurs when symbolic execution encounters an overwhelming number (exponential to the program size) of paths that need to be symbolically reasoned. It severely impacts the scalability and performance of symbolic execution. To tackle this problem, previous works leverage various heuristics to prioritize paths for symbolic execution. They rank the exponential number of paths using static rules or heuristics and explore the paths with the highest rank. However, in practice, these works often fail to generalize to diverse programs. In this work, we propose a novel and effective path prioritization technique with path cover, named Empc. Our key insight is that not all paths need to be symbolically reasoned. Unlike traditional path prioritization, our approach leverages a small subset of paths as a minimum path cover (MPC) that can cover all code regions of the tested programs. To encourage diversity in path prioritization, we compute multiple MPCs. We then guide the search for symbolic execution on the small number of paths inside multiple MPCs rather than the exponential number of paths. We implement our technique Empc based on KLEE. We conduct a comprehensive evaluation of Empc to investigate its performance in code coverage, bug findings, and runtime overhead. The evaluation shows that Empc can cover 19.6% more basic blocks than KLEE's best search strategy and 24.4% more lines compared to the state-of-the-art work cgs. Empc also finds 24 more security violations than KLEE's best search strategy. Meanwhile, Empc can significantly reduce the memory usage of KLEE by up to 93.5%.

Related papers

• PathFuzzing: Worst Case Analysis by Fuzzing Symbolic-Execution Paths [5.1581069235093295]
  Worst-case analysis problem is an optimization-based abstraction of this task.<n> Fuzzing and symbolic execution are widely used techniques for addressing the WCA problem.<n>We propose PathFuzzing, aiming to combine the strengths of both techniques to design a WCA method.
  arXiv  Detail & Related papers  (2025-07-14T03:51:50Z)
• Generating and Understanding Tests via Path-Aware Symbolic Execution with LLMs [8.828992823055]
  PALM is a test generation system that combines symbolic path enumeration with LLM-assisted test generation.<n>Palm helps users better understand path coverage and identify which paths are actually exercised by PALM-generated tests.
  arXiv  Detail & Related papers  (2025-06-24T03:46:16Z)
• Soft Reasoning Paths for Knowledge Graph Completion [63.23109723605835]
  Reasoning paths are reliable information in knowledge graph completion (KGC)<n>In real-world applications, it is difficult to guarantee that computationally affordable paths exist toward all candidate entities.<n>We introduce soft reasoning paths to make the proposed algorithm more stable against missing path circumstances.
  arXiv  Detail & Related papers  (2025-05-06T08:12:48Z)
• Vital: Vulnerability-Oriented Symbolic Execution via Type-Unsafe Pointer-Guided Monte Carlo Tree Search [18.500951309269396]
  This paper proposes a new vulnerability-oriented symbolic execution via type-unsafe pointer-guided Monte Carlo Tree Search (MCTS) We show that Vital could cover up to 90.03% more unsafe pointers and detect up to 37.50% more unique memory errors. In the latter, the results show that Vital could achieve a speedup of up to 30x execution time and a reduction of up to 20x memory consumption.
  arXiv  Detail & Related papers  (2024-08-16T14:29:57Z)
• Multi-Pass Targeted Dynamic Symbolic Execution [0.0]
  We present a Multi-Pass Targeted Dynamic Execution approach that starts from a target program location and moves backward until it reaches a specified entry point. Our approach achieves on average 4X reduction in the number of paths explored and 2X speedup.
  arXiv  Detail & Related papers  (2024-08-14T20:14:59Z)
• Path-optimal symbolic execution of heap-manipulating programs [5.639904484784126]
  This paper introduces POSE, path-optimal symbolic execution, a symbolic execution algorithm that originally accomplishes path optimality against heap-manipulating programs. We formalize the POSE algorithm for a tiny, but representative object-oriented programming language, and implement the formalization into a prototype symbolic executor to experiment the algorithm against a benchmark of sample programs that take data structures as inputs.
  arXiv  Detail & Related papers  (2024-07-23T20:35:33Z)
• Finding Transformer Circuits with Edge Pruning [71.12127707678961]
  We propose Edge Pruning as an effective and scalable solution to automated circuit discovery.<n>Our method finds circuits in GPT-2 that use less than half the number of edges compared to circuits found by previous methods.<n>Thanks to its efficiency, we scale Edge Pruning to CodeLlama-13B, a model over 100x the scale that prior methods operate on.
  arXiv  Detail & Related papers  (2024-06-24T16:40:54Z)
• SLOPE: Search with Learned Optimal Pruning-based Expansion [2.0618817976970103]
  We present the Search with Learned Optimal Pruning-based Expansion (SLOPE) It learns the distance of a node from a possible optimal path, which in turn reduces the size of the open list. This ensures that the search explores only the region close to optimal paths while lowering memory and computational costs.
  arXiv  Detail & Related papers  (2024-06-07T13:42:15Z)
• Parallel Program Analysis on Path Ranges [3.018638214344819]
  Ranged symbolic execution performs symbolic execution on program parts, so called path ranges, in parallel. We present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel.
  arXiv  Detail & Related papers  (2024-02-19T08:26:52Z)
• Path Choice Matters for Clear Attribution in Path Methods [84.29092710376217]
  We introduce textbfConcentration Principle, which allocates high attributions to indispensable features. We then present textbfSAMP, a model-agnostic interpreter, which efficiently searches the near-optimal path. We also propose the infinitesimal constraint (IC) and momentum strategy (MS) to improve the rigorousness and optimality.
  arXiv  Detail & Related papers  (2024-01-19T01:11:44Z)
• Monte-Carlo Tree Search for Multi-Agent Pathfinding: Preliminary Results [60.4817465598352]
  We introduce an original variant of Monte-Carlo Tree Search (MCTS) tailored to multi-agent pathfinding. Specifically, we use individual paths to assist the agents with the the goal-reaching behavior. We also use a dedicated decomposition technique to reduce the branching factor of the tree search procedure.
  arXiv  Detail & Related papers  (2023-07-25T12:33:53Z)
• Coarse-to-Fine Q-attention with Learned Path Ranking [95.00518278458908]
  We propose Learned Path Ranking (LPR), a method that accepts an end-effector goal pose, and learns to rank a set of goal-reaching paths. In addition to benchmarking our approach across 16 RLBench tasks, we also learn real-world tasks, tabula rasa, in 10-15 minutes, with only 3 demonstrations.
  arXiv  Detail & Related papers  (2022-04-04T15:23:14Z)
• GreedyNASv2: Greedier Search with a Greedy Path Filter [70.64311838369707]
  In one-shot NAS methods, the search space is usually considerably huge (eg, $1321$) In this paper, we leverage an explicit path filter to capture the characteristics of paths and directly filter those weak ones. For example, our obtained GreedyNASv2-L achieves $81.1%$ Top-1 accuracy on ImageNet dataset, significantly outperforming the ResNet-50 strong baselines.
  arXiv  Detail & Related papers  (2021-11-24T16:32:29Z)
• ROME: Robustifying Memory-Efficient NAS via Topology Disentanglement and Gradient Accumulation [106.04777600352743]
  Differentiable architecture search (DARTS) is largely hindered by its substantial memory cost since the entire supernet resides in the memory. The single-path DARTS comes in, which only chooses a single-path submodel at each step. While being memory-friendly, it also comes with low computational costs. We propose a new algorithm called RObustifying Memory-Efficient NAS (ROME) to give a cure.
  arXiv  Detail & Related papers  (2020-11-23T06:34:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.