論文の概要: 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標準ライブラリからの計算指向プリミティブ数の間の細分化パッケージと、ブルート力計算によって有限範囲で決定可能な文を自動的に証明する一連の戦術が含まれる。

関連論文リスト

• FPRev: Revealing the Order of Floating-Point Summation by Numerical Testing [5.283916824533212]
  浮動小数点和の順序は数値和の重要な要素である。 本稿では,浮動小数点和の順序を明らかにするアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2024-11-01T08:26:44Z)
• Long Code Arena: a Set of Benchmarks for Long-Context Code Models [75.70507534322336]
  Long Code Arenaは、プロジェクト全体のコンテキストを必要とするコード処理タスクのための6つのベンチマークスイートである。 これらのタスクは、ライブラリベースのコード生成、CIビルドの修復、プロジェクトレベルのコード補完、コミットメッセージ生成、バグローカライゼーション、モジュールの要約といった、コード処理のさまざまな側面をカバーする。 各タスクに対して、テスト用の手作業によるデータセット、評価スイート、オープンソースのベースラインソリューションを提供しています。
  論文  参考訳（メタデータ） (2024-06-17T14:58:29Z)
• Linear-time Minimum Bayes Risk Decoding with Reference Aggregation [52.1701152610258]
  最小ベイズリスク(MBR、Minimum Bayes Risk)は、機械翻訳の品質向上を図ったテキスト生成技術である。 これは2次複雑性を持つ実用計量のペアワイズ計算を必要とする。 本稿では,集約された参照表現に対して計算したスコアを用いて,ペアワイズメトリックスコアを近似する。
  論文  参考訳（メタデータ） (2024-02-06T18:59:30Z)
• ReGAL: Refactoring Programs to Discover Generalizable Abstractions [59.05769810380928]
  Generalizable Abstraction Learning (ReGAL)は、再利用可能な関数のライブラリをコード化して学習する手法である。 ReGALによって発見された共有関数ライブラリは、プログラムが様々な領域で容易に予測できることを示している。 CodeLlama-13Bでは、ReGALはLOGOで11.5%、日付理解で26.1%、TextCraftで8.1%という絶対精度が向上し、3つのドメインのうち2つでGPT-3.5を上回った。
  論文  参考訳（メタデータ） (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)
• Fast Chain-of-Thought: A Glance of Future from Parallel Decoding Leads to Answers Faster [61.83949316226113]
  FastCoTは並列デコーディングに基づくモデルに依存しないフレームワークである。 我々は、FastCoTが通常のアプローチと比較して、無視できる性能低下だけで、推論時間を20%近く削減できることを示します。
  論文  参考訳（メタデータ） (2023-11-14T15:56:18Z)
• Exploring Continual Learning for Code Generation Models [80.78036093054855]
  継続的学習(CL)は、コードドメインの中でまだ過小評価されていない重要な側面である。 コード生成,翻訳,要約,改良など,幅広いタスクをカバーするCodeTask-CLというベンチマークを導入する。 即時選択機構の不安定な訓練により,プロンプトプール (PP) などの有効手法が破滅的な忘れ込みに悩まされることが判明した。
  論文  参考訳（メタデータ） (2023-07-05T16:58:39Z)
• 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)
• openMMF: a library for multimode driven quantum systems [0.0]
  OPENMMFは、離散スペクトルを持つ量子系の時間進化演算子を評価するように設計されている。 このライブラリは、任意のスペクトル組成を持つシステムを研究するための汎用ツールを提供する。
  論文  参考訳（メタデータ） (2020-05-07T12:51:43Z)

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

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