Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries

• URL: http://arxiv.org/abs/2506.09550v3
• Date: Sat, 26 Jul 2025 04:12:15 GMT
• Title: Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries
• Authors: Fanpeng Yang, Xu Ma, Shuling Wang, Xiong Xu, Qinxiang Cao, Naijun Zhan, Xiaofeng Li, Bin Gu,
• Abstract summary: 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.
• Score: 19.23701821549906
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Function summaries, which characterize the behavior of code segments (typically functions) through preconditions and postconditions, are essential for understanding, reusing, and verifying software, particularly in safety-critical domains like aerospace embedded systems. However, these mission-critical legacy code serving as a valuable reused asset often lacks formal specifications. It is challenging to automatically generate function summaries for C programs, due to the existence of complex features such as loops, nested function calls, pointer aliasing, and so on. Moreover, function summaries should support multiple abstraction levels to meet diverse requirements, e.g. precise summaries capturing full functionality for formal verification and intuitive summaries for human understanding. To address these challenges, we first propose a novel framework that combines symbolic execution, large language models (LLMs), and formal verification to generate Relatively Strongest Postconditions (RSPs) and build function summaries that fully capture program behavior. Our approach leverages VST-A's symbolic execution to precisely track program execution paths and state transitions, employs LLMs to infer loop invariants based on predefined templates, and uses Frama-C to guarantee soundness of generated summaries in an iterative refinement loop. Furthermore, from generated RSPs, we automatically synthesize strongest non-redundant postconditions expressed within given domain specific language. We compare our approach with existing work through extensive experiments.

Related papers

• SimStep: Chain-of-Abstractions for Incremental Specification and Debugging of AI-Generated Interactive Simulations [16.00479720281197]
  Chain-of-Abstractions (CoA) is a way to recover programming's core affordances.<n>CoA decomposes the synthesis process into a sequence of cognitively meaningful, task-aligned representations.<n>SimStep is an authoring environment for teachers that scaffolds simulation creation through four intermediate abstractions.
  arXiv  Detail & Related papers  (2025-07-13T14:54:17Z)
• CodeARC: Benchmarking Reasoning Capabilities of LLM Agents for Inductive Program Synthesis [6.8081984950459]
  Large language model agents have shown promise in programming tasks guided by natural language.<n>Existing evaluation protocols rely on static sets of examples and held-out tests.<n>We propose CodeARC, a new evaluation framework where agents interact with a hidden target function.
  arXiv  Detail & Related papers  (2025-03-29T16:50:39Z)
• Learning Task Representations from In-Context Learning [73.72066284711462]
  Large language models (LLMs) have demonstrated remarkable proficiency in in-context learning.<n>We introduce an automated formulation for encoding task information in ICL prompts as a function of attention heads.<n>We show that our method's effectiveness stems from aligning the distribution of the last hidden state with that of an optimally performing in-context-learned model.
  arXiv  Detail & Related papers  (2025-02-08T00:16:44Z)
• EpiCoder: Encompassing Diversity and Complexity in Code Generation [49.170195362149386]
  Existing methods for code generation use code snippets as seed data.<n>We introduce a novel feature tree-based synthesis framework, which revolves around hierarchical code features.<n>Our framework provides precise control over the complexity of the generated code, enabling functionalities that range from function-level operations to multi-file scenarios.
  arXiv  Detail & Related papers  (2025-01-08T18:58:15Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpec is an automated approach to synthesize specifications for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for full proof. It can be successfully applied to verify the programs in a real-world X509-parser project.
  arXiv  Detail & Related papers  (2024-03-31T18:15:49Z)
• From Instructions to Constraints: Language Model Alignment with Automatic Constraint Verification [70.08146540745877]
  We investigate common constraints in NLP tasks, categorize them into three classes based on the types of their arguments. We propose a unified framework, ACT (Aligning to ConsTraints), to automatically produce supervision signals for user alignment with constraints.
  arXiv  Detail & Related papers  (2024-03-10T22:14:54Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  We consider the problem of automatically synthesizing formal specifications from system executions. Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead.
  arXiv  Detail & Related papers  (2023-10-26T14:13:15Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  We characterize several different forms of compositional generalization that are desirable in program synthesis. We propose ExeDec, a novel decomposition-based strategy that predicts execution subgoals to solve problems step-by-step informed by program execution at each step.
  arXiv  Detail & Related papers  (2023-07-26T01:07:52Z)
• Self-regulating Prompts: Foundational Model Adaptation without Forgetting [112.66832145320434]
  We introduce a self-regularization framework for prompting called PromptSRC. PromptSRC guides the prompts to optimize for both task-specific and task-agnostic general representations.
  arXiv  Detail & Related papers  (2023-07-13T17:59:35Z)
• Large Language Models as General Pattern Machines [64.75501424160748]
  We show that pre-trained large language models (LLMs) are capable of autoregressively completing complex token sequences. Surprisingly, pattern completion proficiency can be partially retained even when the sequences are expressed using tokens randomly sampled from the vocabulary. In this work, we investigate how these zero-shot capabilities may be applied to problems in robotics.
  arXiv  Detail & Related papers  (2023-07-10T17:32:13Z)
• Denoising-Contrastive Alignment for Continuous Sign Language Recognition [22.800767994061175]
  Continuous sign language recognition aims to recognize signs in untrimmed sign language videos to textual glosses.<n>Current cross-modality alignment paradigms often neglect the role of textual grammar to guide the video representation.<n>We propose a Denoising-Contrastive Alignment paradigm to enhance video representations.
  arXiv  Detail & Related papers  (2023-05-05T15:20:27Z)
• Summarization Programs: Interpretable Abstractive Summarization with Neural Modular Trees [89.60269205320431]
  Current abstractive summarization models either suffer from a lack of clear interpretability or provide incomplete rationales. We propose the Summarization Program (SP), an interpretable modular framework consisting of an (ordered) list of binary trees. A Summarization Program contains one root node per summary sentence, and a distinct tree connects each summary sentence to the document sentences.
  arXiv  Detail & Related papers  (2022-09-21T16:50:22Z)

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.