SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations

• URL: http://arxiv.org/abs/2606.00220v1
• Date: Fri, 29 May 2026 18:00:06 GMT
• Title: SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
• Abstract summary: SEMBridge generates weakest-precondition and bounded-checking interpretations from the same executable object programs.<n>The Python prototype implements a loop-free imperative core with assignments, conditionals, assumptions, and assertions.
• Score: 0.8557392136621891
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal methods provide rigorous accounts of program behavior, but practical software engineering often works through executable libraries, tests, and incremental design. This paper presents SEMBridge, a small tagless-final framework for generating weakest-precondition and bounded-checking interpretations from the same executable object programs. Instead of committing a program semantics to one abstract syntax tree and then writing separate traversals, object programs are written once against a semantic interface and interpreted into multiple meanings: readable code, concrete execution, predicate transformers, bounded counterexample search, and future proof-assistant or SMT back ends. The Python prototype implements a loop-free imperative core with assignments, conditionals, assumptions, and assertions. Across five example programs, the same tagless-final definitions generated executable state transformers and verification conditions that passed bounded checking over domains up to 729 states. The contribution is not a Scala code-generation system or a new verifier, but a compact architecture for keeping executable semantics, weakest-precondition artifacts, and bounded validation synchronized.

Related papers

• Technical Report: A Formal Semantics for Java Symbolic Evaluation using Large-Block Encoding [0.9985222473972001]
  Symbolic execution is used to find bugs, generate test cases, and provide correctness guarantees.<n>Java Ranger is a path-merging tool for Java programs that progressively transforms imperative Java code toward the language of formal logic.<n>We formalize each of these transformations and prove their soundness with respect to a simplified version of the Java concrete semantics.
  arXiv  Detail & Related papers  (2026-08-05T06:49:28Z)
• FlowSeg: Dynamic Semantic Guidance for LLM-Conditioned Segmentation [76.08991871243333]
  FlowSeg introduces semantic guidance via a bidirectional semantic flow between intermediate decoding states and condition embeddings.<n>This design yields semantically grounded mask representations and visually aligned language conditions, enabling more reliable matching.
  arXiv  Detail & Related papers  (2026-05-28T06:55:35Z)
• Misquoted No More: Securely Extracting F* Programs with IO [0.3848364262836075]
  Shallow embeddings that use monads to represent effects are popular in proof-oriented languages.<n>Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C.<n>We build on this idea, but limit the use of translation validation to a first extraction step.
  arXiv  Detail & Related papers  (2026-02-23T15:37:18Z)
• zkStruDul: Programming zkSNARKs with Structural Duality [0.2449909275410287]
  zkStruDul is a language that unifies input transformations and predicate definitions into a single combined abstraction.<n>We provide a source-level semantics and prove its behavior is identical to the projected semantics, allowing straightforward standard reasoning.
  arXiv  Detail & Related papers  (2025-11-13T18:06:21Z)
• Text2Mem: A Unified Memory Operation Language for Memory Operating System [59.082901444153684]
  We introduce Text2Mem, a unified memory operation language for model agents.<n>Text2Mem provides a standardized pathway from natural correctness reliable execution.
  arXiv  Detail & Related papers  (2025-09-14T07:30:09Z)
• Correctness-Guaranteed Code Generation via Constrained Decoding [11.531496728670746]
  We present a constrained runtime decoding algorithm for generating semantically correct programs.<n>We show that our method can generate semantically correct programs conforming to any prescribed scripting API.<n>We further show that, with careful design, our semantic guarantees extend to correctness, as validated in the application of generating game mechanics for a roguelike video game.
  arXiv  Detail & Related papers  (2025-08-20T20:48:18Z)
• 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)
• Code Representation Pre-training with Complements from Program Executions [29.148208436656216]
  We propose FuzzPretrain to explore the dynamic information of programs revealed by their test cases and embed it into the feature representations of code as complements. FuzzyPretrain yielded more than 6%/9% mAP improvements on code search over its counterparts trained with only source code or AST.
  arXiv  Detail & Related papers  (2023-09-04T01:57:22Z)
• A Static Evaluation of Code Completion by Large Language Models [65.18008807383816]
  Execution-based benchmarks have been proposed to evaluate functional correctness of model-generated code on simple programming problems. static analysis tools such as linters, which can detect errors without running the program, haven't been well explored for evaluating code generation models. We propose a static evaluation framework to quantify static errors in Python code completions, by leveraging Abstract Syntax Trees.
  arXiv  Detail & Related papers  (2023-06-05T19:23:34Z)
• Outline, Then Details: Syntactically Guided Coarse-To-Fine Code Generation [61.50286000143233]
  ChainCoder is a program synthesis language model that generates Python code progressively. A tailored transformer architecture is leveraged to jointly encode the natural language descriptions and syntactically aligned I/O data samples.
  arXiv  Detail & Related papers  (2023-04-28T01:47:09Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  We propose a retrieval-augmented code completion framework, leveraging both lexical copying and referring to code with similar semantics by retrieval. We evaluate our approach in the code completion task in Python and Java programming languages, achieving a state-of-the-art performance on CodeXGLUE benchmark.
  arXiv  Detail & Related papers  (2022-03-15T08:25:08Z)
• 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)

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.