論文の概要: 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 14:37:47.827810
• 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:
• 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万以上の検証条件を示す。 我々は、和や配列の証明にも重要なステップを確立する。

関連論文リスト

• Verified invertible lexer using regular expressions and DFAs [0.0]
  本稿では,シリアライズおよびレキシングフレームワークに適用する可逆性の概念について検討する。 シリアライゼーションはデータ構造をビット配列に書き込むプロセスであり、レキシングは文字のストリームを読み取ってトークンに分割するプロセスである。
  論文  参考訳（メタデータ） (2024-12-18T08:03:17Z)
• NoviCode: Generating Programs from Natural Language Utterances by Novices [59.71218039095155]
  初心者非プログラマによるAPIと自然言語記述を入力とする新しいNLプログラミングタスクであるNoviCodeを提示する。 我々は、NoviCodeがコード合成領域における挑戦的なタスクであることを示し、非技術的命令から複雑なコードを生成することは、現在のText-to-Codeパラダイムを超えている。
  論文  参考訳（メタデータ） (2024-07-15T11:26:03Z)
• 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)
• Structured Chain-of-Thought Prompting for Code Generation [48.43888515848583]
  CoTプロンプト(Chain-of-Thought)は最先端のプロンプト技術である。 本研究では、構造化CoT(Structured CoTs)を提案し、コード生成のための新しいプロンプト技術であるSCoTプロンプトを提案する。
  論文  参考訳（メタデータ） (2023-05-11T06:43:37Z)
• 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)
• Verified Reversible Programming for Verified Lossless Compression [11.020543186794459]
  ロスレス圧縮の実装は通常、エンコーダとデコーダの2つのプログラムを含む。 我々は、非対称数値システム(ANS)に基づく圧縮手法のかなりのクラスが、エンコーダとデコーダの間で共有構造を持つことを観察する。 私たちはAgdaに埋め込まれた小さな可逆言語「Flipper」を実装しました。
  論文  参考訳（メタデータ） (2022-11-02T16:39:41Z)
• On Sparsifying Encoder Outputs in Sequence-to-Sequence Models [90.58793284654692]
  我々はTransformerをテストベッドとして、エンコーダとデコーダの間にあるゲートの層を導入します。 ゲートは、パリシティ誘導L0ペナルティの期待値を用いて正規化される。 このスペーサー化が2つの機械翻訳と2つの要約タスクに与える影響について検討する。
  論文  参考訳（メタデータ） (2020-04-24T16:57:52Z)

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

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