論文の概要: SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations

• arxiv url: http://arxiv.org/abs/2606.00220v1
• Date: Fri, 29 May 2026 18:00:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-02 21:34:28.164371
• Title: SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
• Title（参考訳）: SEMBridge: Weakest-PreconditionとBunded-Checking Interpretationsによるタグレスフィールドプログラムセマンティックス
• Abstract要約: SEMBridgeは、同じ実行可能なオブジェクトプログラムから最も弱い条件と境界チェックの解釈を生成する。 Pythonプロトタイプは、割り当て、条件、仮定、アサーションを備えたループフリーな命令コアを実装している。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 形式的手法はプログラムの振舞いの厳密な説明を提供するが、実用的なソフトウェア工学は実行可能なライブラリ、テスト、インクリメンタルな設計を通じて機能することが多い。 本稿では,SEMBridgeを提案する。SEMBridgeは,同じ実行可能オブジェクトプログラムから,最弱条件と境界チェックの解釈を生成するための,タグレスファイナルフレームワークである。 プログラムセマンティクスを1つの抽象構文木にコミットし、別々のトラバーサルを書く代わりに、オブジェクトプログラムはセマンティクスインターフェースに対して一度記述され、読みやすいコード、具体的な実行、述語変換、境界付き反例探索、将来の証明補助またはSMTバックエンドといった複数の意味に解釈される。 Pythonプロトタイプは、割り当て、条件、仮定、アサーションを備えたループフリーな命令コアを実装している。 5つのサンプルプログラムで、同じタグレスファイナル定義が実行可能状態変換器と検証条件を生成し、729状態まで境界チェックをパスした。 コントリビューションはScalaのコード生成システムや新しい検証ツールではなく、実行可能なセマンティクス、最も弱い条件のアーティファクト、境界付きバリデーションを同期するコンパクトなアーキテクチャである。

関連論文リスト

• Technical Report: A Formal Semantics for Java Symbolic Evaluation using Large-Block Encoding [0.9985222473972001]
  シンボリック実行はバグを見つけ、テストケースを生成し、正確性を保証するために使用される。 Java Rangerは、命令型Javaコードを形式論理の言語に段階的に変換するJavaプログラムのためのパスマージツールである。 これらの変換を形式化し、Javaの具体的セマンティクスの簡易バージョンに関して、それらの健全性を証明します。
  論文  参考訳（メタデータ） (2026-08-05T06:49:28Z)
• FlowSeg: Dynamic Semantic Guidance for LLM-Conditioned Segmentation [76.08991871243333]
  FlowSegは、中間復号状態と条件埋め込みの間の双方向のセマンティックフローを通じてセマンティックガイダンスを導入する。 この設計は意味的に接地されたマスク表現と視覚的に整合した言語条件をもたらし、より信頼性の高いマッチングを可能にする。
  論文  参考訳（メタデータ） (2026-05-28T06:55:35Z)
• Misquoted No More: Securely Extracting F* Programs with IO [0.3848364262836075]
  効果を表すモナドを使用する浅層埋め込みは、証明指向言語で人気がある。 浅い組込みプログラムが検証されると、しばしばOCamlやCのような主流言語に抽出される。 私たちはこのアイデアに基づいていますが、翻訳バリデーションの使用を最初の抽出ステップに制限します。
  論文  参考訳（メタデータ） (2026-02-23T15:37:18Z)
• zkStruDul: Programming zkSNARKs with Structural Duality [0.2449909275410287]
  zkStruDulは、入力変換を統一し、定義を単一の複合抽象化に述語する言語である。 我々は、ソースレベルのセマンティクスを提供し、その振る舞いが予測されたセマンティクスと同一であることを証明する。
  論文  参考訳（メタデータ） (2025-11-13T18:06:21Z)
• Text2Mem: A Unified Memory Operation Language for Memory Operating System [59.082901444153684]
  モデルエージェントのための統一メモリ操作言語であるText2Memを紹介する。 Text2Memは、自然な正確性を保証するための標準化されたパスを提供する。
  論文  参考訳（メタデータ） (2025-09-14T07:30:09Z)
• Correctness-Guaranteed Code Generation via Constrained Decoding [11.531496728670746]
  本稿では,意味論的に正しいプログラムを生成するための制約付き実行時復号アルゴリズムを提案する。 提案手法は,任意の所定のスクリプティングAPIに従って,意味的に正しいプログラムを生成することができることを示す。 さらに、慎重に設計することで、我々のセマンティック保証が正当性にまで拡張され、ローグライクなビデオゲームにゲームメカニクスを発生させることで検証されることを示す。
  論文  参考訳（メタデータ） (2025-08-20T20:48:18Z)
• Weakly Supervised Semantic Parsing with Execution-based Spurious Program Filtering [19.96076749160955]
  本稿では,プログラムの実行結果に基づくドメインに依存しないフィルタリング機構を提案する。 私たちはこれらの表現に対して多数決を行い、他のプログラムと大きく異なる意味を持つプログラムを特定し、フィルタリングします。
  論文  参考訳（メタデータ） (2023-11-02T11:45:40Z)
• Code Representation Pre-training with Complements from Program Executions [29.148208436656216]
  テストケースで明らかになったプログラムの動的情報を調べ,それを補体としてコードの特徴表現に埋め込むために,FuzzPretrainを提案する。 FuzzyPretrainは、ソースコードやASTのみをトレーニングしたコード検索に対して、6%/9%のmAP改善を実現した。
  論文  参考訳（メタデータ） (2023-09-04T01:57:22Z)
• A Static Evaluation of Code Completion by Large Language Models [65.18008807383816]
  単純なプログラミング問題に対するモデル生成コードの機能的正当性を評価するために,実行ベースベンチマークが提案されている。 プログラムを実行せずにエラーを検出するlinterのような静的解析ツールは、コード生成モデルを評価するために十分に研究されていない。 抽象構文木を利用して,Pythonのコード補完における静的エラーを定量化する静的評価フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-06-05T19:23:34Z)
• Outline, Then Details: Syntactically Guided Coarse-To-Fine Code Generation [61.50286000143233]
  ChainCoderは、Pythonコードを段階的に生成するプログラム合成言語モデルである。 自然言語記述と構文的に整合したI/Oデータサンプルを共同で符号化するために、カスタマイズされたトランスフォーマーアーキテクチャを利用する。
  論文  参考訳（メタデータ） (2023-04-28T01:47:09Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。 我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2022-03-15T08:25:08Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  プログラム合成エンジンにおける部分的なプログラム表現手法について紹介する。 モジュラーニューラルネットワークとして実装された近似実行モデルを学ぶ。 これらのハイブリッドニューロシンボリック表現は、実行誘導型シンセサイザーがより強力な言語構成を使うことができることを示す。
  論文  参考訳（メタデータ） (2020-12-23T20:40:18Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。