Array-Carrying Symbolic Execution for Function Contract Generation

• URL: http://arxiv.org/abs/2602.23216v2
• Date: Fri, 27 Feb 2026 07:55:17 GMT
• Title: Array-Carrying Symbolic Execution for Function Contract Generation
• Authors: Weijie Lu, Jingyu Ke, Hongfei Fu, Zhouyue Sun, Yi Zhou, Guoqiang Li, Haokun Li,
• Abstract summary: We propose a novel symbolic execution framework that carries invariants and assigns information over contiguous segments of arrays.<n>We implement our framework as a prototype within LLVM, and further integrate our prototype with the ACSL assertion format and the Frama-C software verification platform.
• Score: 4.472707897843483
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is fundamental in inter-procedural analysis where properties of functions are first obtained via the generation of function contracts and then the generated contracts are used as building blocks to analyze the whole program. Typical objectives in function contract generation include pre-/post-conditions and assigns information (that specifies the modification information over program variables and memory segments during function execution). In programs with array manipulations, a crucial point in function contract generation is the treatment of array segments that imposes challenges in inferring invariants and assigns information over such segments. To address this challenge, we propose a novel symbolic execution framework that carries invariants and assigns information over contiguous segments of arrays. We implement our framework as a prototype within LLVM, and further integrate our prototype with the ACSL assertion format and the Frama-C software verification platform. Experimental evaluation over a variety of benchmarks from the literature and functions from realistic libraries shows that our framework is capable of handling array manipulating functions that indeed involve the carry of array information and are beyond existing approaches.

Related papers

• Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries [19.23701821549906]
  We propose a novel framework that combines symbolic execution, large language models (LLMs), and formal verification to generate Relatively Strongest Postconditions (RSPs)<n>Our approach leverages VST-A's symbolic execution to precisely track program execution paths and state transitions.<n>From generated RSPs, we automatically synthesize strongest non-redundant postconditions expressed within given domain specific language.
  arXiv  Detail & Related papers  (2025-06-11T09:33:02Z)
• Beyond the Edge of Function: Unraveling the Patterns of Type Recovery in Binary Code [55.493408628371235]
  We propose ByteTR, a framework for recovering variable types in binary code.<n>In light of the ubiquity of variable propagation across functions, ByteTR conducts inter-procedural analysis to trace variable propagation and employs a gated graph neural network to capture long-range data flow dependencies for variable type recovery.
  arXiv  Detail & Related papers  (2025-03-10T12:27:05Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages.<n>This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• C Analyzer : A Static Program Analysis Tool for C Programs [0.0]
  C Analyzer is a tool developed for static analysis of C programs. This project work tries to leverage Abstract Interpretation techniques for static analysis of C programs.
  arXiv  Detail & Related papers  (2024-01-28T11:43:16Z)
• UniRef++: Segment Every Reference Object in Spatial and Temporal Spaces [92.52589788633856]
  We propose UniRef++ to unify the four reference-based object segmentation tasks with a single architecture. With the unified designs, UniRef++ can be jointly trained on a broad range of benchmarks and can flexibly complete multiple tasks at run-time. Our proposed UniRef++ achieves state-of-the-art performance on RIS and RVOS, and performs competitively on FSS and VOS with a parameter-shared network.
  arXiv  Detail & Related papers  (2023-12-25T12:54:11Z)
• Multi-level Reasoning for Robotic Assembly: From Sequence Inference to Contact Selection [74.40109927350856]
  We present the Part Assembly Sequence Transformer (PAST) to infer assembly sequences from a target blueprint. We then use a motion planner and optimization to generate part movements and contacts. Experimental results show that our approach generalizes better than prior methods.
  arXiv  Detail & Related papers  (2023-12-17T00:47:13Z)
• FIND: A Function Description Benchmark for Evaluating Interpretability Methods [86.80718559904854]
  This paper introduces FIND (Function INterpretation and Description), a benchmark suite for evaluating automated interpretability methods. FIND contains functions that resemble components of trained neural networks, and accompanying descriptions of the kind we seek to generate. We evaluate methods that use pretrained language models to produce descriptions of function behavior in natural language and code.
  arXiv  Detail & Related papers  (2023-09-07T17:47:26Z)
• Better Context Makes Better Code Language Models: A Case Study on Function Call Argument Completion [15.068025336990287]
  We show that existing code completion models do not yield good results on our completion task. We query a program analyzer for information relevant to a given function call, and consider ways to provide the analyzer results to different code completion models during inference and training. Our experiments show that providing access to the function implementation and function usages greatly improves the argument completion performance.
  arXiv  Detail & Related papers  (2023-06-01T06:25:58Z)
• A Mechanistic Interpretation of Arithmetic Reasoning in Language Models using Causal Mediation Analysis [128.0532113800092]
  We present a mechanistic interpretation of Transformer-based LMs on arithmetic questions. This provides insights into how information related to arithmetic is processed by LMs.
  arXiv  Detail & Related papers  (2023-05-24T11:43:47Z)
• An Algorithm and Complexity Results for Causal Unit Selection [16.307996243413967]
  Unit selection problem aims to identify objects, called units, that are most likely to exhibit a desired mode of behavior when subjected to stimuli. We propose the first exact algorithm for finding optimal units given a broad class of causal objective functions and a fully specified structural causal model.
  arXiv  Detail & Related papers  (2023-02-28T08:46:51Z)
• 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)
• Discrete Signal Processing with Set Functions [6.548580592686076]
  We derive discrete-set signal processing (SP), a novel shift-invariant linear signal processing framework for set functions. SP considers different notions of shift obtained from set union and difference operations. We show two applications and experiments: compression in submodular function optimization and sampling for preference elicitation in auctions.
  arXiv  Detail & Related papers  (2020-01-28T12:19:57Z)

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.