論文の概要: UTC Time, Formally Verified
- arxiv url: http://arxiv.org/abs/2209.14227v2
- Date: Wed, 13 Dec 2023 18:04:55 GMT
- ステータス: 処理完了
- システム内更新日: 2023-12-14 21:31:04.084960
- Title: UTC Time, Formally Verified
- Title(参考訳): UTC 時刻,形式的検証
- Authors: Ana de Almeida Borges, Mireia Gonz\'alez Bedmar, Juan Conejero
Rodr\'iguez, Eduardo Hermo Reyes, Joaquim Casals Bu\~nuel and Joost J.
Joosten
- Abstract要約: FV Timeは、Coqの証明アシスタントでMathematical Componentsライブラリを使って開発された小さな検証プロジェクトである。
これは、時間形式(UTCとタイムスタンプ)間の変換を管理するためのライブラリであり、時間演算の一般的な機能である。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: FV Time is a small-scale verification project developed in the Coq proof
assistant using the Mathematical Components libraries. It is a library for
managing conversions between time formats (UTC and timestamps), as well as
commonly used functions for time arithmetic. As a library for time conversions,
its novelty is the implementation of leap seconds, which are part of the UTC
standard but usually not implemented in existing libraries. Since the verified
functions of FV Time are reasonably simple yet non-trivial, it nicely
illustrates our methodology for verifying software with Coq.
In this paper we present a description of the project, emphasizing the main
problems faced while developing the library, as well as some general-purpose
solutions that were produced as by-products and may be used in other
verification projects. These include a refinement package between
proof-oriented MathComp numbers and computation-oriented primitive numbers from
the Coq standard library, as well as a set of tactics to automatically prove
certain decidable statements over finite ranges through brute-force
computation.
- Abstract(参考訳): FV Timeは、Coqの証明アシスタントでMathematical Componentsライブラリを使って開発された小さな検証プロジェクトである。
これは、時間形式(UTCとタイムスタンプ)間の変換を管理するためのライブラリであり、時間演算の一般的な機能である。
時間変換のライブラリとして、その新規性はUTC標準の一部であるが、既存のライブラリでは実装されない跳躍秒の実装である。
FV Time の検証機能は合理的に単純だが非自明であるため,Coq によるソフトウェア検証の方法論をうまく説明している。
本稿では,ライブラリ開発中に直面した主な問題点を強調するとともに,副産物として開発され,他の検証プロジェクトでも使用可能な汎用ソリューションについて述べる。
これには、証明指向のmathcomp数とcoq標準ライブラリからの計算指向プリミティブ数の間の細分化パッケージと、ブルート力計算によって有限範囲で決定可能な文を自動的に証明する一連の戦術が含まれる。
関連論文リスト
- Active Learning of Mealy Machines with Timers [0.0]
タイマーを用いた一般機械の問合せ学習のための最初のアルゴリズムを提案する。
我々のアルゴリズムはVaandragerらのL#アルゴリズムを時間設定に拡張したものである。
Rustで書かれたプロトタイプ実装の実験は、我々のアルゴリズムがリアルなベンチマークを効率的に学習できることを示しています。
論文 参考訳(メタデータ) (2024-03-04T13:20:52Z) - Linear-time Minimum Bayes Risk Decoding with Reference Aggregation [61.63208012250885]
最小ベイズリスク(MBR、Minimum Bayes Risk)は、機械翻訳の品質向上を図ったテキスト生成技術である。
これは2次複雑性を持つ実用計量のペアワイズ計算を必要とする。
本稿では,集約された参照表現に対して計算したスコアを用いて,ペアワイズメトリックスコアを近似する。
論文 参考訳(メタデータ) (2024-02-06T18:59:30Z) - ReGAL: Refactoring Programs to Discover Generalizable Abstractions [66.37493420911979]
Generalizable Abstraction Learning (ReGAL)は、コードカプセル化によって再利用可能な関数のライブラリを学ぶ方法である。
ReGALによって発見された共有関数ライブラリは、プログラムが様々な領域で容易に予測できることを示している。
CodeLlama-13Bでは、ReGALはグラフィックスで11.5%、日付理解で26.1%、MinecraftベースのテキストゲームであるTextCraftで8.1%という絶対的な精度向上を実現している。
論文 参考訳(メタデータ) (2024-01-29T18:45:30Z) - The role of library versions in Developer-ChatGPT conversations [1.6252311034292488]
4000以上のDeveloper-ChatGPTインタラクションのデータセットであるDevGPTを分析する。
コード関連の会話でライブラリのバージョン制約が言及される頻度を定量化します。
論文 参考訳(メタデータ) (2024-01-29T17:46:18Z) - Constant-Time Wasmtime, for Real This Time: End-to-End Verified Zero-Overhead Constant-Time Programming for the Web and Beyond [2.803675461772196]
本稿ではJITスタイルのWasmtimeをベースとした新しいコンパイラ検証スイートを提案する。
また、ct-wasmをターゲットに、既存の定時対応DSLである FaCT のポートも提示する。
論文 参考訳(メタデータ) (2023-11-24T01:38:19Z) - Exploring Continual Learning for Code Generation Models [80.78036093054855]
継続的学習(CL)は、コードドメインの中でまだ過小評価されていない重要な側面である。
コード生成,翻訳,要約,改良など,幅広いタスクをカバーするCodeTask-CLというベンチマークを導入する。
即時選択機構の不安定な訓練により,プロンプトプール (PP) などの有効手法が破滅的な忘れ込みに悩まされることが判明した。
論文 参考訳(メタデータ) (2023-07-05T16:58:39Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳(メタデータ) (2023-06-27T17:05:32Z) - TASTY: A Transformer based Approach to Space and Time complexity [0.4724825031148411]
コードベース言語モデル(LM)は、ソフトウェア工学の分野で非常に有望な結果を示している。
複数の言語にまたがるコードスニペットのラベル付きデータセットを作成します。
私たちは、コードから空間の複雑さを見つけるのにLMを使うことを提案しています。
論文 参考訳(メタデータ) (2023-05-06T03:37:44Z) - Program of Thoughts Prompting: Disentangling Computation from Reasoning
for Numerical Reasoning Tasks [108.4568236569645]
CoT(Chain-of-thinkts prompting)は、これらのタスクに対する最先端の手法である。
本稿では、言語モデルを用いて推論過程をプログラムとして表現する「思考プログラム(PoT)」を提案する。
PoTは、評価されたすべてのデータセットに対して、CoTに対する平均的なパフォーマンス向上を約12%示すことができる。
論文 参考訳(メタデータ) (2022-11-22T21:06:00Z) - Coded Distributed Computing with Partial Recovery [56.08535873173518]
部分回復型符号化計算(CCPR)と呼ばれる新しい符号化行列ベクトル乗法を導入する。
CCPRは計算時間と復号化の複雑さを減らし、精度と計算速度のトレードオフを可能にする。
次に、この手法をより一般的な計算タスクの分散実装に拡張し、部分的回復を伴う符号化通信方式を提案する。
論文 参考訳(メタデータ) (2020-07-04T21:34:49Z) - openMMF: a library for multimode driven quantum systems [0.0]
OPENMMFは、離散スペクトルを持つ量子系の時間進化演算子を評価するように設計されている。
このライブラリは、任意のスペクトル組成を持つシステムを研究するための汎用ツールを提供する。
論文 参考訳(メタデータ) (2020-05-07T12:51:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。