Path-optimal symbolic execution of heap-manipulating programs

• URL: http://arxiv.org/abs/2407.16827v1
• Date: Tue, 23 Jul 2024 20:35:33 GMT
• Title: Path-optimal symbolic execution of heap-manipulating programs
• Authors: Pietro Braione, Giovanni Denaro,
• Abstract summary: 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.
• Score: 5.639904484784126
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Symbolic execution is at the core of many techniques for program analysis and test generation. Traditional symbolic execution of programs with numeric inputs enjoys the property of forking as many analysis traces as the number of analyzed program paths, a property that in this paper we refer to as path optimality. On the contrary, current approaches for symbolic execution of heap-manipulating programs fail to satisfy this property, thereby incurring heavy path explosion effects that crucially penalize the efficiency of the analysis. 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. Our experiments provide initial empirical evidence of the potential of POSE for improving on the state of the art of symbolic execution of heap-manipulating programs.

Related papers

• 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)
• Weakly Supervised Semantic Parsing with Execution-based Spurious Program Filtering [19.96076749160955]
  We propose a domain-agnostic filtering mechanism based on program execution results. We run a majority vote on these representations to identify and filter out programs with significantly different semantics from the other programs.
  arXiv  Detail & Related papers  (2023-11-02T11:45:40Z)
• Divide, Conquer and Verify: Improving Symbolic Execution Performance [0.14999444543328289]
  Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. We present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects.
  arXiv  Detail & Related papers  (2023-10-05T15:21:10Z)
• Searching for More Efficient Dynamic Programs [61.79535031840558]
  We describe a set of program transformations, a simple metric for assessing the efficiency of a transformed program, and a search procedure to improve this metric. We show that in practice, automated search can find substantial improvements to the initial program.
  arXiv  Detail & Related papers  (2021-09-14T20:52:55Z)
• Latent Execution for Neural Program Synthesis Beyond Domain-Specific Languages [97.58968222942173]
  We take the first step to synthesize C programs from input-output examples. In particular, we propose La Synth, which learns the latent representation to approximate the execution of partially generated programs. We show that training on these synthesized programs further improves the prediction performance for both Karel and C program synthesis.
  arXiv  Detail & Related papers  (2021-06-29T02:21:32Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jl is an extendable symbolic system which uses dynamic multiple dispatch to change behavior depending on the domain needs. We show that by formalizing a generic API on actions independent of implementation, we can retroactively add optimized data structures to our system. We demonstrate the ability to swap between classical term-rewriting simplifiers and e-graph-based term-rewriting simplifiers.
  arXiv  Detail & Related papers  (2021-05-09T14:22:43Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  We introduce a technique for representing partially written programs in a program synthesis engine. We learn an approximate execution model implemented as a modular neural network. We show that these hybrid neuro-symbolic representations enable execution-guided synthesizers to use more powerful language constructs.
  arXiv  Detail & Related papers  (2020-12-23T20:40:18Z)
• An AI-Assisted Design Method for Topology Optimization Without Pre-Optimized Training Data [68.8204255655161]
  An AI-assisted design method based on topology optimization is presented, which is able to obtain optimized designs in a direct way. Designs are provided by an artificial neural network, the predictor, on the basis of boundary conditions and degree of filling as input data.
  arXiv  Detail & Related papers  (2020-12-11T14:33:27Z)
• Symbolic Parallel Adaptive Importance Sampling for Probabilistic Program Analysis [9.204612164524947]
  Probabilistic software analysis aims at quantifying the probability of a target event occurring during the execution of a program. We present SYMbolic Parallel Adaptive Importance Sampling (SYMPAIS), a new inference method tailored to analyze path conditions generated from the symbolic execution of programs.
  arXiv  Detail & Related papers  (2020-10-10T17:39:12Z)
• Process Discovery for Structured Program Synthesis [70.29027202357385]
  A core task in process mining is process discovery which aims to learn an accurate process model from event log data. In this paper, we propose to use (block-) structured programs directly as target process models. We develop a novel bottom-up agglomerative approach to the discovery of such structured program process models.
  arXiv  Detail & Related papers  (2020-08-13T10:33:10Z)

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.