Fugu-MT 論文翻訳(概要): Type-level Property Based Testing

論文の概要: Type-level Property Based Testing

arxiv url: http://arxiv.org/abs/2407.12726v1
Date: Wed, 17 Jul 2024 16:43:41 GMT
ステータス: 処理完了
システム内更新日: 2024-07-18 16:16:05.207422
Title: Type-level Property Based Testing
Title（参考訳）: タイプレベルプロパティベースのテスト
Authors: Thomas Ekström Hansen, Edwin Brady,
Abstract要約: 本稿では,ソフトウェア仕様と依存型付けモデル,コンパイル時の実装の結合を統一する自動フレームワークを提案する。いくつかの興味深いシステムやネットワークプロトコルをモデル化し、型チェッカーで実装が指定された動作であることを検証し、モデルが仕様のセマンティクスにマッチしていることをテストすることができます。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by-nc-nd/4.0/
Abstract: We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.
Abstract（参考訳）: 本稿では,ソフトウェア仕様と依存型付きモデル,コンパイル時の実装の結合を統一する自動フレームワークを提案する。モデルチェックと型チェックは現在、プログラムの正確性を自動的に検証する別の技術である。 Property Based Testing (PBT)、Indexed State Monads (ISMs)、および依存型を使用して、いくつかの興味深いシステムやネットワークプロトコルをモデル化し、型チェッカーに、実装が指定通りに振る舞うことを確認し、モデルが仕様のセマンティクスにマッチすることをテストさせます。

関連論文リスト

Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing [0.3807314298073301]
有限状態オートマトン方言を用いて指定されたサービスアプリケーションを実現するため、tt CAREと呼ばれる分散ランタイムアプリケーションが導入された。 tt CAREの形式的モデリング、検証、テストについて詳述する。
論文参考訳（メタデータ） (2025-01-22T15:03:25Z)
SYNTHEVAL: Hybrid Behavioral Testing of NLP Models with Synthetic CheckLists [59.08999823652293]
我々は,NLPモデルの包括的評価のために,SyntheVALを提案する。最後の段階では、人間の専門家が困難な例を調査し、手動でテンプレートを設計し、タスク固有のモデルが一貫して示す障害の種類を特定します。我々は、感情分析と有害言語検出という2つの分類課題にSynTHEVALを適用し、これらの課題における強力なモデルの弱点を特定するのに、我々のフレームワークが有効であることを示す。
論文参考訳（メタデータ） (2024-08-30T17:41:30Z)
Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
ショッピング・バスケット・アプリケーション・モデルにおけるPrism Model Checkerを用いたシミュレーションの結果を示す。目的は、買い物客が買い物プロセスの多くの定義された状態を通過するときの行動をシミュレートすることである。
論文参考訳（メタデータ） (2023-07-16T00:14:40Z)
Zero-shot Model Diagnosis [80.36063332820568]
ディープラーニングモデルを評価するための一般的なアプローチは、興味のある属性を持つラベル付きテストセットを構築し、そのパフォーマンスを評価することである。本稿では,ゼロショットモデル診断(ZOOM)がテストセットやラベル付けを必要とせずに可能であることを論じる。
論文参考訳（メタデータ） (2023-03-27T17:59:33Z)
Language Model Cascades [72.18809575261498]
テスト時に1つのモデルで繰り返し対話する、あるいは複数のモデルの合成は、さらに機能を拡張する。制御フローと動的構造を持つ場合、確率的プログラミングのテクニックが必要となる。この観点から、スクラッチパッド/思考連鎖、検証器、STaR、選択推論、ツール利用など、いくつかの既存のテクニックを定式化します。
論文参考訳（メタデータ） (2022-07-21T07:35:18Z)
On the Limits of Evaluating Embodied Agent Model Generalization Using Validation Sets [101.28658250723804]
本稿では,より広い視野を効果的に活用し,次のステップでナビゲーションや操作を行うかを選択するモジュールによるトランスフォーマーモデルの拡張実験を行う。提案したモジュールは改良され,実際に,一般的なベンチマークデータセットであるALFREDの未確認検証セット上での最先端のパフォーマンスが向上した。この結果は、機械学習タスクではより広い現象かもしれないが、主にテストスプリットの評価を制限するベンチマークでのみ顕著である、と我々は考えているので強調する。
論文参考訳（メタデータ） (2022-05-18T23:52:21Z)
Lifted Model Checking for Relational MDPs [12.574454799055026]
pCTL-REBELは、リレーショナルMDP上のpCTL特性を検証するためのリフトモデルチェック手法である。 pCTLモデル検査手法は, 無限領域であっても, リレーショナルMDPに対して決定可能であることを示す。
論文参考訳（メタデータ） (2021-06-22T13:12:36Z)
DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
変数モデル(例えば、特徴モデル)は、ソフトウェアアーティファクトの変数と共通性を表現する一般的な方法である。複雑でしばしば大規模な機能モデルは欠陥になりうる、すなわち、ソフトウェアアーチファクトの期待される変動特性を表現しない。
論文参考訳（メタデータ） (2021-02-11T11:22:20Z)
Interpretable Entity Representations through Large-Scale Typing [61.4277527871572]
本稿では,人間の読みやすいエンティティ表現を作成し,箱から高パフォーマンスを実現する手法を提案する。我々の表現は、微粒な実体型に対する後続確率に対応するベクトルである。特定のドメインに対して,学習に基づく方法で,型セットのサイズを縮小できることを示す。
論文参考訳（メタデータ） (2020-04-30T23:58:03Z)
An Automated Approach for the Discovery of Interoperability [0.0]
標準フォーマットでモデルを交換しても形状特性の保存は保証されないことを示す。 CAD-to-CAEおよび/またはCAD-to-CAMインタラクション上での相互運用試験に拡張することができる。
論文参考訳（メタデータ） (2020-01-26T06:07:43Z)

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