Fugu-MT 論文翻訳(概要): Advances of Proof Scores in CafeOBJ

論文の概要: Advances of Proof Scores in CafeOBJ

arxiv url: http://arxiv.org/abs/2112.10373v3
Date: Wed, 6 Dec 2023 07:31:18 GMT
ステータス: 処理完了
システム内更新日: 2023-12-07 19:58:35.707788
Title: Advances of Proof Scores in CafeOBJ
Title（参考訳）: CafeOBJにおける証明スコアの進歩
Authors: Kokichi Futatsugi
Abstract要約: CafeOBJは実行可能な代数的仕様言語システムである。本稿では,CafeOBJの仕様検証における証明スコアの進歩について述べる。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by-nc-nd/4.0/
Abstract: Critical flaws continue to exist at the level of domain, requirement, and/or design specification, and specification verification (i.e., to check whether a specification has desirable properties) is still one of the most important challenges in software/system engineering. CafeOBJ is an executable algebraic specification language system and domain/requirement/design engineers can write proof scores for improving quality of specifications by the specification verification. This paper describes advances of the proof scores for the specification verification in CafeOBJ.
Abstract（参考訳）: 重要な欠陥は、ドメイン、要件、および/または設計仕様のレベルで存在し続け、仕様の検証(つまり、仕様が望ましい特性を持っているかどうかをチェックする)は、ソフトウェア/システムエンジニアリングにおいて依然として最も重要な課題の1つです。 CafeOBJは実行可能な代数的仕様言語システムであり、ドメイン/要求/設計エンジニアは仕様検証によって仕様の品質を向上させるための証明スコアを書くことができる。本稿では,CafeOBJの仕様検証における証明の進歩について述べる。

関連論文リスト

KaPQA: Knowledge-Augmented Product Question-Answering [59.096607961704656]
我々はAdobe AcrobatとPhotoshop製品に焦点を当てた2つのQAデータセットを紹介した。また、製品QAタスクにおけるモデルの性能を高めるために、新しい知識駆動型RAG-QAフレームワークを提案する。
論文参考訳（メタデータ） (2024-07-22T22:14:56Z)
A Graphics Function Standard Specification Validator [0.0]
標準グラフィックス関数の自然言語ソフトウェア仕様に対して検証手法を提案し,実装した。チェックは、一貫性、完全性、データ要素と関数記述の曖昧さの欠如のために行われる。
論文参考訳（メタデータ） (2024-01-31T04:54:17Z)
Selene: Pioneering Automated Proof in Software Verification [62.09555413263788]
実世界の産業レベルのマイクロカーネルであるseL4をベースとした,最初のプロジェクトレベルの自動証明ベンチマークであるSeleneを紹介する。 GPT-3.5-turbo や GPT-4 のような先進的な大規模言語モデル (LLM) による実験結果から, 自動証明生成領域における LLM の機能を強調した。
論文参考訳（メタデータ） (2024-01-15T13:08:38Z)
Validation of Rigorous Requirements Specifications and Document Automation with the ITLingo RSL Language [0.0]
ITLingoイニシアチブは、技術的文書の厳密さと一貫性を高めるためにRSLという要求仕様言語を導入した。本稿では、要求検証と文書自動化の分野における既存の研究・ツールについてレビューする。我々は、カスタマイズされたチェックと、RSL自体で動的に定義された言語規則に基づいて、仕様の検証によりRSLを拡張することを提案する。
論文参考訳（メタデータ） (2023-12-17T21:39:26Z)
Klever: Verification Framework for Critical Industrial C Programs [0.0]
我々は,大規模かつ重要な産業用Cプログラムに自動ソフトウェア検証ツールを適用する労力を削減するために,Kleverソフトウェア検証フレームワークを提案する。既存のツールは、環境モデリング、要件の仕様、ターゲットプログラムの多くのバージョンと構成の検証、検証結果のエキスパートアセスメントなど、広く採用されている手段を提供していない。
論文参考訳（メタデータ） (2023-09-28T13:23:59Z)
Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security [0.0]
メモリ管理の誤った仕様と実装は、システムのクラッシュや悪用可能な攻撃につながる可能性がある。本稿では,実世界のOSにおける並列メモリ管理の最初の正式な仕様と機構的証明について述べる。
論文参考訳（メタデータ） (2023-09-17T03:41:10Z)
Validation-Driven Development [54.50263643323]
本稿では,形式的開発における要件の検証を優先する検証駆動開発(VDD)プロセスを紹介する。 VDDプロセスの有効性は、航空業界におけるケーススタディを通じて実証されている。
論文参考訳（メタデータ） (2023-08-11T09:15:26Z)
Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
論文参考訳（メタデータ） (2023-01-05T18:18:46Z)
ProQA: Structural Prompt-based Pre-training for Unified Question Answering [84.59636806421204]
ProQAは統一されたQAパラダイムであり、単一のモデルによって様々なタスクを解決する。全てのQAタスクの知識一般化を同時にモデル化し、特定のQAタスクの知識カスタマイズを維持します。 ProQAは、フルデータの微調整、数ショットの学習、ゼロショットテストシナリオの両方のパフォーマンスを一貫して向上させる。
論文参考訳（メタデータ） (2022-05-09T04:59:26Z)
Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。 AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
論文参考訳（メタデータ） (2021-09-25T22:53:24Z)

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