Parallel Program Analysis on Path Ranges
- URL: http://arxiv.org/abs/2402.11938v2
- Date: Thu, 16 May 2024 13:35:35 GMT
- Title: Parallel Program Analysis on Path Ranges
- Authors: Jan Haltermanna, Marie-Christine Jakobs, Cedric Richter, Heike Wehrheim,
- Abstract summary: 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.
- Score: 3.018638214344819
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Symbolic execution is a software verification technique symbolically running programs and thereby checking for bugs. Ranged symbolic execution performs symbolic execution on program parts, so called path ranges, in parallel. Due to the parallelism, verification is accelerated and hence scales to larger programs. In this paper, we discuss a generalization of ranged symbolic execution to arbitrary program analyses. More specifically, we present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel. Our approach in particular allows to run different analyses on different program parts. We have implemented this generalization on top of the tool CPAchecker and evaluated it on programs from the SV-COMP benchmark. Our evaluation shows that verification can benefit from the parallelisation of the verification task, but also needs a form of work stealing (between analyses) as to become efficient
Related papers
- To CoT or not to CoT? Chain-of-thought helps mainly on math and symbolic reasoning [55.52872152909785]
Chain-of-thought (CoT) via prompting is the de facto method for eliciting reasoning capabilities from large language models (LLMs)
We show that CoT gives strong performance benefits primarily on tasks involving math or logic, with much smaller gains on other types of tasks.
arXiv Detail & Related papers (2024-09-18T17:55:00Z) - Scaling Symbolic Execution to Large Software Systems [0.0]
Symbolic execution is a popular static analysis technique used both in program verification and in bug detection software.
We focus on an error finding framework called the Clang Static Analyzer, and the infrastructure built around it named CodeChecker.
arXiv Detail & Related papers (2024-08-04T02:54:58Z) - 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) - 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) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
Learned transpilation offers an alternative to manual re-writing and engineering efforts.
Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness.
Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
arXiv Detail & Related papers (2023-09-25T15:42:18Z) - Improved Tree Search for Automatic Program Synthesis [91.3755431537592]
A key element is being able to perform an efficient search in the space of valid programs.
Here, we suggest a variant of MCTS that leads to state of the art results on two vastly different DSLs.
arXiv Detail & Related papers (2023-03-13T15:09:52Z) - QParallel: Explicit Parallelism for Programming Quantum Computers [62.10004571940546]
We present a language extension for parallel quantum programming.
QParallel removes ambiguities concerning parallelism in current quantum programming languages.
We introduce a tool that guides programmers in the placement of parallel regions by identifying the subroutines that profit most from parallelization.
arXiv Detail & Related papers (2022-10-07T16:35:16Z) - Learning from Self-Sampled Correct and Partially-Correct Programs [96.66452896657991]
We propose to let the model perform sampling during training and learn from both self-sampled fully-correct programs and partially-correct programs.
We show that our use of self-sampled correct and partially-correct programs can benefit learning and help guide the sampling process.
Our proposed method improves the pass@k performance by 3.1% to 12.3% compared to learning from a single reference program with MLE.
arXiv Detail & Related papers (2022-05-28T03:31:07Z) - 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) - Benchmarking Symbolic Execution Using Constraint Problems -- Initial
Results [6.961253535504978]
Symbolic execution is a powerful technique for bug finding and program testing.
We transform CSP benchmarks into C programs suitable for testing the reasoning capabilities of symbolic execution tools.
arXiv Detail & Related papers (2020-01-22T08:48:55Z)
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.