論文の概要: ESBMC-Python: A Bounded Model Checker for Python Programs

• arxiv url: http://arxiv.org/abs/2407.03472v1
• Date: Wed, 3 Jul 2024 19:38:14 GMT
• ステータス: 処理完了
• システム内更新日: 2024-07-08 20:00:48.306495
• Title: ESBMC-Python: A Bounded Model Checker for Python Programs
• Title（参考訳）: ESBMC-Python:Pythonプログラムのバウンドモデルチェッカー
• Authors: Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho, Youcheng Sun, Lucas C. Cordeiro,
• Abstract要約: 本稿では,Pythonプログラムの検証ツールを紹介する。 入力プログラムを抽象構文木に変換し、型情報を推論し追加する。 この記述を、満足度モジュラー理論の解法を用いて評価された公式に変換する。
• 参考スコア（独自算出の注目度）: 8.980206368890013
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification.
• Abstract（参考訳）: 本稿では,型アノテーションとフロントエンド処理を用いて,境界モデルチェック(BMC)パイプラインの機能を利用するPythonプログラムの検証ツールを提案する。 入力プログラムを抽象構文木に変換し、型情報を推論し追加する。 そして、Pythonの式とステートメントを中間表現に変換する。 最後に、この記述を満足度変調理論(SMT)の解法で評価された公式に変換する。 提案手法は、効率的なSMTベースの有界モデルチェッカー(ESBMC)によって実現され、その結果、最初のBMCベースのPythonコード検証ツールであるESBMC-Pythonと呼ばれるツールが生まれた。 この目的のために特別に開発したテストスイートによる実験結果から,試験が成功し,失敗した場合の有効性が示された。 さらに、Ethereum Consensus Specificationで本当の問題を見つけた。

関連論文リスト

• Chat-like Asserts Prediction with the Support of Large Language Model [34.140962210930624]
  我々は,Pythonプロジェクトで有意義なアサート文を生成するために,Chatライクな実行ベースのアサート予測(tool)を導入する。 ツールはペルソナ、Chain-of-Thought、ワンショットの学習技術を利用して、迅速な設計を行い、LLMやPythonインタプリタと通信する。 評価の結果, 単一アサーション文生成では64.7%, 全体アサーション文生成では62%の精度が得られた。
  論文  参考訳（メタデータ） (2024-07-31T08:27:03Z)
• pyvene: A Library for Understanding and Improving PyTorch Models via Interventions [79.72930339711478]
  $textbfpyvene$は、さまざまなPyTorchモジュールに対するカスタマイズ可能な介入をサポートするオープンソースライブラリである。 私たちは、$textbfpyvene$が、ニューラルモデルへの介入を実行し、他のモデルとインターバルされたモデルを共有するための統一されたフレームワークを提供する方法を示します。
  論文  参考訳（メタデータ） (2024-03-12T16:46:54Z)
• arfpy: A python package for density estimation and generative modeling with adversarial random forests [1.3597551064547502]
  本稿では,適応ランダムフォレスト(ARF)のピソン実装である$textitarfpy$を紹介する(Watson et al., 2023)。 これは、与えられたデータに似た新しいデータを合成するための軽量な手順である。
  論文  参考訳（メタデータ） (2023-11-13T14:28:21Z)
• Noisy Pair Corrector for Dense Retrieval [59.312376423104055]
  ノイズペアコレクタ(NPC)と呼ばれる新しい手法を提案する。 NPCは検出モジュールと修正モジュールから構成される。 我々は,テキスト検索ベンチマークのNatural QuestionとTriviaQA,コード検索ベンチマークのStaQCとSO-DSで実験を行った。
  論文  参考訳（メタデータ） (2023-11-07T08:27:14Z)
• SPRINT: A Unified Toolkit for Evaluating and Demystifying Zero-shot Neural Sparse Retrieval [92.27387459751309]
  ニューラルスパース検索を評価するための統一PythonツールキットであるSPRINTを提供する。 我々は、よく認識されているベンチマークBEIRにおいて、強く再現可能なゼロショットスパース検索ベースラインを確立する。 SPLADEv2は、元のクエリとドキュメントの外で、ほとんどのトークンでスパース表現を生成する。
  論文  参考訳（メタデータ） (2023-07-19T22:48:02Z)
• PyVBMC: Efficient Bayesian inference in Python [8.924669503280333]
  PyVBMCは、後方およびモデル推論のための変分ベイズモンテカルロ (VBMC) アルゴリズムのPython実装である。 VBMCは、モデル評価が軽度から極端に高価である場合に、効率的なパラメータ推定とモデル評価のために設計されている。
  論文  参考訳（メタデータ） (2023-03-16T17:37:22Z)
• PyHHMM: A Python Library for Heterogeneous Hidden Markov Models [63.01207205641885]
  PyHHMM は Heterogeneous-Hidden Markov Models (HHMM) のオブジェクト指向Python実装である。 PyHHMMは、異種観測モデル、データ推論の欠如、異なるモデルの順序選択基準、半教師付きトレーニングなど、同様のフレームワークではサポートされない機能を強調している。 PyHHMMは、numpy、scipy、scikit-learn、およびシーボーンPythonパッケージに依存しており、Apache-2.0ライセンスの下で配布されている。
  論文  参考訳（メタデータ） (2022-01-12T07:32:36Z)
• Program Synthesis with Large Language Models [40.41120807053989]
  我々はPythonにおけるプログラム合成のための大規模言語モデルを評価する。 合成性能はモデルサイズと対数的にスケールすることがわかった。 最高のモデルでさえ、特定の入力を与えられたプログラムの出力を予測できないことが分かりました。
  論文  参考訳（メタデータ） (2021-08-16T03:57:30Z)
• Using Python for Model Inference in Deep Learning [0.6027358520885614]
  pythonで推論を実行しながら、パフォーマンスとパッケージングの制約を満たす方法を示します。 複数のPythonインタプリタを単一のプロセスで使用して,スケーラブルな推論を実現する方法を提案する。
  論文  参考訳（メタデータ） (2021-04-01T04:48:52Z)
• pyBART: Evidence-based Syntactic Transformations for IE [52.93947844555369]
  pyBARTは、英語のUD木を拡張UDグラフに変換するためのオープンソースのPythonライブラリである。 パターンに基づく関係抽出のシナリオで評価すると、より少ないパターンを必要としながら、より高精細なUDよりも高い抽出スコアが得られる。
  論文  参考訳（メタデータ） (2020-05-04T07:38:34Z)
• OPFython: A Python-Inspired Optimum-Path Forest Classifier [68.8204255655161]
  本稿では,OPFythonと表記されるPythonベースのOptimum-Path Forestフレームワークを提案する。 OPFythonはPythonベースのライブラリなので、C言語よりもフレンドリーな環境とプロトタイピングの作業スペースを提供する。
  論文  参考訳（メタデータ） (2020-01-28T15:46:19Z)

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

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