論文の概要: Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study

• arxiv url: http://arxiv.org/abs/2412.07235v1
• Date: Tue, 10 Dec 2024 06:54:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-11 22:09:45.259165
• Title: Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
• Title（参考訳）: ASN.1/ACNエンコーダとデコーダの形式検証
• Authors: Mario Bucev, Samuel Chassot, Simon Felix, Filip Schramka, Viktor Kunčak,
• Abstract要約: ASN.1は地上および宇宙通信で広く使われているデータ構造を記述するための言語である。 ACN は ASN.1 に沿って、複雑なバイナリフォーマットとレガシプロトコルを記述するために使用できる。 ASN.1/ACNコードジェネレータをScalaコードに移植する方法を示す。 次に、生成元を拡張して、実行可能コードだけでなく、十分な事前条件、後条件、帰納的証明のための補題を出力します。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: We propose a verified executable Scala backend for ASN1SCC, a compiler for ASN.1/ACN. ASN.1 is a language for describing data structures widely employed in ground and space telecommunications. ACN can be used along ASN.1 to describe complex binary formats and legacy protocols. To avoid error-prone and time-consuming manual writing of serializers, we show how to port an ASN.1/ACN code generator to generate Scala code. We then enhance the generator to emit not only the executable code but also strong enough pre-conditions, post-conditions, and lemmas for inductive proofs. This allowed us to verify the resulting generated annotated code using Stainless, a program verifier for Scala. The properties we prove include the absence of runtime errors, such as out-of-bound accesses or divisions by zero. For the base library, we also prove the invertibility of the decoding and encoding functions, showing that decoding yields the encoded value back. Furthermore, our system automatically inserts invertibility proofs for arbitrary records in the generated code, proving over 300'000 verification conditions. We establish key steps towards such proofs for sums and arrays as well.
• Abstract（参考訳）: ASN.1/ACN のコンパイラである ASN1SCC に対して,検証可能な Scala バックエンドを提案する。 ASN.1は地上および宇宙通信で広く使われているデータ構造を記述するための言語である。 ACN は ASN.1 に沿って、複雑なバイナリフォーマットとレガシプロトコルを記述するために使用できる。 シリアライザのエラーが発生しやすく、時間を要する手書き記述を避けるため、ASN.1/ACNコードジェネレータをScalaコードに移植する方法を示す。 次に、生成元を拡張して、実行可能コードだけでなく、十分な事前条件、後条件、帰納的証明のための補題を出力します。 これにより、Scalaのプログラム検証ツールであるstensを使って、生成されたアノテーション付きコードを検証できます。 私たちが証明したプロパティには、アウトオブバウンドアクセスや0の除算のようなランタイムエラーがないことが含まれています。 基本ライブラリに対しては,復号化関数と復号化関数の可逆性を証明し,復号化関数が復号化値を返すことを示す。 さらに,生成したコード中の任意のレコードに対する可逆性証明を自動的に挿入し,300万以上の検証条件を示す。 我々は、和や配列の証明にも重要なステップを確立する。

関連論文リスト

• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.4779196219827508]
  組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。 我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
  論文  参考訳（メタデータ） (2025-04-23T18:04:38Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  大規模言語モデル(LLM)はコードの形式的な側面をモデル化しないため、コンパイル不可能な出力を生成する。 本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。 提案手法は,コンパイルエラーを半分以上削減し,コード合成,翻訳,修復作業における機能的正しさを向上する。
  論文  参考訳（メタデータ） (2025-04-12T15:03:00Z)
• KodCode: A Diverse, Challenging, and Verifiable Synthetic Dataset for Coding [49.56049319037421]
  KodCodeは、高品質で検証可能なトレーニングデータを取得するという永続的な課題に対処する、合成データセットである。 自己検証手順によって体系的に検証される質問解決テスト三つ子を含む。 このパイプラインは大規模で堅牢で多様なコーディングデータセットを生成する。
  論文  参考訳（メタデータ） (2025-03-04T19:17:36Z)
• Verified invertible lexer using regular expressions and DFAs [0.0]
  本稿では,シリアライズおよびレキシングフレームワークに適用する可逆性の概念について検討する。 シリアライゼーションはデータ構造をビット配列に書き込むプロセスであり、レキシングは文字のストリームを読み取ってトークンに分割するプロセスである。
  論文  参考訳（メタデータ） (2024-12-18T08:03:17Z)
• Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
  大規模言語モデル(LLM)は、多くのソフトウェアエンジニアリング活動において有望であることを示している。 本稿では,分離論理に基づく仕様生成におけるOpenAIのGPTモデルの有効性について検討する。
  論文  参考訳（メタデータ） (2024-11-04T17:44:11Z)
• Decoding at the Speed of Thought: Harnessing Parallel Decoding of Lexical Units for LLMs [57.27982780697922]
  大規模言語モデルは、自然言語の理解と生成において例外的な能力を示した。 しかし、それらの生成速度は、その復号過程の本質的にシーケンシャルな性質によって制限される。 本稿では,データ駆動方式で実装された新しいデコーディング手法であるLexical Unit Decodingを紹介する。
  論文  参考訳（メタデータ） (2024-05-24T04:35:13Z)
• SparseCoder: Identifier-Aware Sparse Transformer for File-Level Code Summarization [51.67317895094664]
  本稿では,大規模なソースコードプロジェクトの理解と維持を支援するファイルレベルのコード要約について検討する。 長いコードシーケンスを効果的に処理するための識別子対応スパース変換器であるSparseCoderを提案する。
  論文  参考訳（メタデータ） (2024-01-26T09:23:27Z)
• Using LLM such as ChatGPT for Designing and Implementing a RISC Processor: Execution,Challenges and Limitations [11.07566083431614]
  この論文は、解析、トークン化、エンコーディング、アテンションメカニズム、コード生成時のトークンとイテレーションのサンプリングなど、関連するステップについてレビューする。 RISCコンポーネントの生成されたコードは、FPGA基板上でテストベンチとハードウェア実装によって検証される。
  論文  参考訳（メタデータ） (2024-01-18T20:14:10Z)
• VerilogEval: Evaluating Large Language Models for Verilog Code Generation [6.88526119890374]
  本稿では,VerilogインストラクショナルWebサイトHDLBitsの156問題からなる総合評価データセットを提案する。 評価セットは、単純な組合せ回路から複雑な有限状態マシンまで、様々なVerilogコード生成タスクからなる。
  論文  参考訳（メタデータ） (2023-09-14T09:15:34Z)
• ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers [60.6418431624873]
  大きな言語モデル(LLM)は、機能記述からコードを実装するのに優れているが、アルゴリズムの問題に悩まされている。 我々は,アルゴリズムプログラムを LLM 生成 Oracle で合成するフレームワーク ALGO を提案し,その生成をガイドし,その正確性を検証する。 実験の結果,ALGOを装着すると,Codexモデルよりも8倍,CodeTよりも2.6倍の1サブミッションパス率が得られることがわかった。
  論文  参考訳（メタデータ） (2023-05-24T00:10:15Z)
• Neuro-symbolic Zero-Shot Code Cloning with Cross-Language Intermediate Representation [13.881954273779403]
  我々は,従来のプログラミング言語のコードに対して意味論的に類似したクローンを学習することなく発見するタスクに対処する,ニューロシンボリックなアプローチを定義した。 CodeNetデータセットで利用可能なC言語ペアのSBT IRによるコードクローンタスクに対して、クロスプログラミング言語検索の最高のパフォーマンスモデルであるUnixCoderを微調整する。 この微調整されたUnixCoderでは、CodeNetから合成されたテストスプリットに基づいて、事前訓練されたUnixCoderモデルに対して12.85 MAP@2のパフォーマンスが改善される。
  論文  参考訳（メタデータ） (2023-04-26T07:41:26Z)
• Python Code Generation by Asking Clarification Questions [57.63906360576212]
  本稿では,この課題に対して,より斬新で現実的なセットアップを導入する。 我々は、自然言語記述の過小評価は、明確化を問うことで解決できると仮定する。 我々は、生成した合成明確化質問と回答を含む自然言語記述とコードのペアを含む、CodeClarQAという新しいデータセットを収集し、導入する。
  論文  参考訳（メタデータ） (2022-12-19T22:08:36Z)
• On Sparsifying Encoder Outputs in Sequence-to-Sequence Models [90.58793284654692]
  我々はTransformerをテストベッドとして、エンコーダとデコーダの間にあるゲートの層を導入します。 ゲートは、パリシティ誘導L0ペナルティの期待値を用いて正規化される。 このスペーサー化が2つの機械翻訳と2つの要約タスクに与える影響について検討する。
  論文  参考訳（メタデータ） (2020-04-24T16:57:52Z)

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

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