Syntax-driven Incremental Program Verification of Matching Logic Properties

• URL: http://arxiv.org/abs/2606.08824v1
• Date: Sun, 07 Jun 2026 20:32:37 GMT
• Title: Syntax-driven Incremental Program Verification of Matching Logic Properties
• Abstract summary: We present an approach to the incremental verification of programs written in KernelC.<n>The approach is based on a syntactic-semantic framework that enables analyzing code chunks in isolation.<n>Results show that our approach does not penalize the efficiency of formal verification and can outperform program re-verification after changes.
• Score: 36.861969535480526
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Incrementality is a fundamental design principle to master the complexity of large, long-lived software systems. This principle has been embraced by agile development processes and it lays at the base of continuous software evolution. A major challenge in this context is to incrementally re-verify the correctness of software artifacts after every change, focusing the verification efforts only on the parts affected by the change. We present an approach to the incremental verification of programs written in KernelC, annotated with properties expressed in matching logic. The approach is based on a syntactic-semantic framework that enables analyzing code chunks in isolation so that, after a change to a program fragment, only the part whose semantics is affected by the change is re-processed. This property is obtained by expressing the language syntax through an operator precedence grammar and by formalizing its semantics through a synthesized attribute schema. We have implemented our technique in a prototype tool and experimentally evaluated its effectiveness. The results show that our approach does not penalize the efficiency of formal verification and can outperform program re-verification after changes, depending on the presence and type of annotations, as well as the position of the change and the program structure.

Related papers

• Is Code Better Than Language for Algorithmic Reasoning [58.86873062890482]
  We show that for tool-augmented language models, comparing natural-language reasoning with code-execution pipelines is difficult because the comparison changes both the intermediate representation and the execution mechanism.<n>We separate these factors with an intermediate intervention: the model expresses its reasoning as executable code, and the language model simulates that code in context to produce an answer.<n>We observe that the intermediate intervention is not meaningfully different from natural-language reasoning (+0.15pp)
  arXiv  Detail & Related papers  (2026-06-14T04:17:21Z)
• AlgoTouch: An Execution-Centered Approach to Incremental Construction of Imperative Programs [0.0]
  AlgoTouch is an execution-based system for incremental construction of imperative programs.<n>It relies on an explicit notional machine that exposes data storage, computation, and control flow.<n>AlgoTouch automatically generates correct and readable programs in Python, C, C++, and Java.
  arXiv  Detail & Related papers  (2026-06-02T08:57:49Z)
• SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation [6.0174402828965725]
  SpecAlign is a framework for semantic evaluation and refinement of SystemVerilog Assertions.<n>We show that SpecAlign effectively detects semantic inconsistencies and improves assertion alignment without relying on golden RTL.
  arXiv  Detail & Related papers  (2026-05-24T17:22:09Z)
• What Really Improves Mathematical Reasoning: Structured Reasoning Signals Beyond Pure Code [72.9921566968371]
  We revisit the claim that code improves reasoning through controlled pretraining experiments on a 10T-token corpus with fine-grained domain separation.<n>Code substantially improves programming ability but does not act as a general reasoning enhancer.<n>Cross-domain structured reasoning traces, such as code-text and math-text mixtures, are better explained.
  arXiv  Detail & Related papers  (2026-05-19T12:37:01Z)
• Governed Metaprogramming for Intelligent Systems: Reclassifying Eval as a Governed Effect [0.0]
  We present governed metaprogramming, a language design where programrepresentations are first-class values.<n>We prove three properties: purity of form manipulation, the no-bypass theorem, and boundary preservation.<n>The central contribution is reclassifying eval from a language primitive into a governed effect.
  arXiv  Detail & Related papers  (2026-05-05T02:56:43Z)
• Multi-Agent Procedural Graph Extraction with Structural and Logical Refinement [66.51979814832332]
  model formulates procedural graph extraction as a multi-round reasoning process with dedicated structural and logical refinement.<n>Experiments demonstrate that model achieves substantial improvements in both structural correctness and logical consistency over strong baselines.
  arXiv  Detail & Related papers  (2026-01-27T04:00:48Z)
• Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
  Speculative decoding accelerates autoregressive language model inference by verifying multiple draft tokens in parallel.<n>Existing sparsification methods are designed primarily for standard token-by-token autoregressive decoding.<n>We propose a sparse verification framework that jointly sparsifies attention, FFN, and MoE components during the verification stage to reduce the dominant computation cost.
  arXiv  Detail & Related papers  (2025-12-26T07:53:41Z)
• How Different Tokenization Algorithms Impact LLMs and Transformer Models for Binary Code Analysis [0.0]
  Despite its significance, tokenization in the context of assembly code remains an underexplored area.<n>We explore preprocessing customization options and pre-tokenization rules tailored to the unique characteristics of assembly code.<n>We compare tokenizers based on tokenization efficiency, vocabulary compression, and representational fidelity for assembly code.
  arXiv  Detail & Related papers  (2025-11-05T19:45:26Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• Inferring Attributed Grammars from Parser Implementations [1.0217990949413291]
  We introduce a novel approach for inferring attributed grammars from implementations of input grammars.<n>By observing runtime executions and mapping the program's behavior to the grammar, we systematically extract and embed semantic actions into the grammar rules.<n>We demonstrate the feasibility of our approach using an initial set of programs, showing that it can accurately reproduce program behavior through the generated attributed grammars.
  arXiv  Detail & Related papers  (2025-07-17T13:32:59Z)
• Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
  We explore the use of consistency between the output programs for related inputs to reduce the impact of spurious programs. We find that a more consistent formalism leads to improved model performance even without consistency-based training.
  arXiv  Detail & Related papers  (2021-07-13T03:48:04Z)

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.