論文の概要: Unlocking the Power of Environment Assumptions for Unit Proofs
- arxiv url: http://arxiv.org/abs/2409.12269v1
- Date: Wed, 18 Sep 2024 19:01:30 GMT
- ステータス: 処理完了
- システム内更新日: 2024-11-07 15:38:21.198398
- Title: Unlocking the Power of Environment Assumptions for Unit Proofs
- Title（参考訳）: 単位証明における環境消費の力の解き放つ
- Authors: Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel,
- Abstract要約: vMocksは、コードレベルの形式検証を行うときに有効な環境を特定するための直感的なフレームワークを提供する。
我々は、SEAMOCKと呼ばれるCプログラムの検証のためのvMockライブラリを実装した。
- 参考スコア（独自算出の注目度）: 0.03171448182742677
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Clearly articulating the assumptions of the execution environment is crucial for the successful application of code-level formal verification. The process of specifying a model for the environment can be both laborious and error-prone, often requiring domain experts. In contrast, when engineers write unit tests, they frequently employ mocks (tMocks) to define the expected behavior of the environment in which the function under test operates. These tMocks describe how the environment behaves, e.g., the return types of an external API call (stateless behaviour) or the correct sequence of function calls (stateful behaviour). Mocking frameworks have proven to be highly effective tools for crafting unit tests. In our work, we draw inspiration from tMocks and introduce their counterpart in the realm of formal verification, which we term vMocks. vMocks offer an intuitive framework for specifying a plausible environment when conducting code-level formal verification. We implement a vMock library for the verification of C programs called SEAMOCK. We investigate the practicality of vMocks by, first, comparing specifications styles in the communication layer of the Android Trusty Trusted Execution Environment (TEE) open source project, and second, in the verification of mbedTLS, a widely used open source C library that provides secure communication protocols and cryptography primitives for embedded systems. Based on our experience, we conclude that vMocks complement other forms of environment models. We believe that vMocks ease adoption of code-level formal verification among developers already familiar with tMocks.
- Abstract（参考訳）: コードレベルの形式検証を成功させるためには、明らかに実行環境の仮定を明確に述べることが不可欠である。
環境のためのモデルを指定するプロセスは、退屈でエラーを起こしやすいため、しばしばドメインの専門家を必要とします。
対照的に、エンジニアがユニットテストを書く際には、しばしばモック(tMocks)を使用して、テスト対象の関数が動作する環境の期待される振る舞いを定義します。
これらのtMockは、例えば、外部API呼び出し(ステートレスな振る舞い)の戻りタイプや、関数呼び出し(ステートフルな振る舞い)の正しいシーケンスなど、環境がどのように振る舞うかを記述します。
モッキングフレームワークは単体テストを作るのに非常に効果的なツールであることが証明されている。
我々の研究では、tMocksからインスピレーションを得て、vMocksと呼ばれる形式的検証の領域でそれに対応するものを紹介します。
vMocksは、コードレベルの形式検証を行うときに有効な環境を特定するための直感的なフレームワークを提供する。
我々は、SEAMOCKと呼ばれるCプログラムの検証のためのvMockライブラリを実装した。
第1に,Android Trusty Trusted Execution Environment (TEE) オープンソースプロジェクトの通信層における仕様スタイルを比較し,第2に,組込みシステムにセキュアな通信プロトコルと暗号プリミティブを提供する,広く使用されているオープンソースCライブラリ mbedTLS の検証を行った。
我々の経験から、vMocksは他の形態の環境モデルを補完するものであると結論付けている。
私たちは、すでにtMocksに精通している開発者の間で、vMocksがコードレベルの形式検証の採用を容易にしてくれると信じています。
関連論文リスト
- Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
Code-Development Benchmark (Codev-Bench)は、細粒度で現実世界、リポジトリレベル、開発者中心の評価フレームワークです。
Codev-Agentは、リポジトリのクローリングを自動化し、実行環境を構築し、既存のユニットテストから動的呼び出しチェーンを抽出し、データ漏洩を避けるために新しいテストサンプルを生成するエージェントベースのシステムである。
論文 参考訳（メタデータ） (2024-10-02T09:11:10Z) - On the Impacts of Contexts on Repository-Level Code Generation [5.641402231731082]
リポジトリレベルのコード生成を評価するために設計された新しいベンチマークである textbfmethodnamews を提案する。
実行可能性、包括的なテストケース生成による機能的正当性、ファイル間のコンテキストの正確な利用という3つの重要な側面に注目します。
論文 参考訳（メタデータ） (2024-06-17T10:45:22Z) - On The Importance of Reasoning for Context Retrieval in Repository-Level Code Editing [82.96523584351314]
我々は、コンテキスト検索のタスクをリポジトリレベルのコード編集パイプラインの他のコンポーネントと分離する。
我々は、推論が収集された文脈の精度を向上させるのに役立っているが、それでもその十分性を識別する能力は欠如していると結論づける。
論文 参考訳（メタデータ） (2024-06-06T19:44:17Z) - Comments as Natural Logic Pivots: Improve Code Generation via Comment Perspective [85.48043537327258]
本稿では, MANGO (comMents As Natural loGic pivOts) を提案する。
その結果、MANGOは強いベースラインに基づいてコードパス率を大幅に改善することがわかった。
論理的なコメントの復号化戦略の堅牢性は、考えの連鎖よりも顕著に高い。
論文 参考訳（メタデータ） (2024-04-11T08:30:46Z) - An In-Context Learning Agent for Formal Theorem-Proving [10.657173216834668]
我々は、LeanやCoqのような環境で、形式的定理コンテキストのためのコンテキスト内学習エージェントを提示します。
COPRAは大規模言語モデルに対して、ステートフルなバックトラック検索から戦術的応用を提案することを何度も求めている。
我々はCompCertプロジェクトのMiniF2FベンチマークとCoqタスクセットに対するCOPRAの実装を評価した。
論文 参考訳（メタデータ） (2023-10-06T16:21:22Z) - (Security) Assertions by Large Language Models [25.270188328436618]
セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。
我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
論文 参考訳（メタデータ） (2023-06-24T17:44:36Z) - Guiding Language Models of Code with Global Context using Monitors [17.05416012014561]
コード(LM)の言語モデルは、周囲のコードが十分なコンテキストを提供するときにうまく機能します。
LMはそのようなグローバルな文脈に対する認識が限られ、幻覚に陥る。
そこで我々は,モニタが静的解析を用いて復号を導出する,モニタ誘導復号法(MGD)を提案する。
論文 参考訳（メタデータ） (2023-06-19T08:13:50Z) - Learning Label Modular Prompts for Text Classification in the Wild [56.66187728534808]
そこで本研究では,非定常学習/テスト段階の異なるテキスト分類手法を提案する。
複雑なタスクをモジュラー成分に分解することで、そのような非定常環境下での堅牢な一般化が可能になる。
テキスト分類タスクのためのラベルモジュール型プロンプトチューニングフレームワークMODcularPROMPTを提案する。
論文 参考訳（メタデータ） (2022-11-30T16:26:38Z) - Mimicking Production Behavior with Generated Mocks [11.367562045401554]
実運用環境でのアプリケーションを監視して,モックによる現実的な実行シナリオを模倣するテストを生成することを提案する。
このアプローチは自動化され、RICKと呼ばれるオープンソースのツールで実装されている。
生成されたテストケースはすべて実行可能であり、52.4%は本番環境で観測されたターゲットメソッドの完全な実行コンテキストをうまく模倣している。
論文 参考訳（メタデータ） (2022-08-02T09:08:18Z) - Language Models as Zero-Shot Planners: Extracting Actionable Knowledge
for Embodied Agents [111.33545170562337]
自然言語で表現された高レベルなタスクを、選択された実行可能なステップのセットに基底付ける可能性について検討する。
事前学習したLMが十分に大きく、適切に誘導された場合、ハイレベルなタスクを効果的に低レベルな計画に分解できることがわかった。
本稿では,既存の実演の条件を規定し,計画が許容可能な行動に意味的に変換される手順を提案する。
論文 参考訳（メタデータ） (2022-01-18T18:59:45Z) - Neighbor-view Enhanced Model for Vision and Language Navigation [78.90859474564787]
視覚と言語ナビゲーション(VLN)では、エージェントが自然言語の指示に従うことによって、ターゲットの場所へナビゲートする必要がある。
本研究では,隣接するビューから視覚的コンテキストを適応的に組み込むマルチモジュールNeighbor-View Enhanced Model (NvEM)を提案する。
論文 参考訳（メタデータ） (2021-07-15T09:11:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。