論文の概要: Petrify: Petri-net Based Analysis of Concurrency Properties in Java Bytecode
- arxiv url: http://arxiv.org/abs/2607.00830v1
- Date: Wed, 01 Jul 2026 11:52:40 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-02 19:56:07.880234
- Title: Petrify: Petri-net Based Analysis of Concurrency Properties in Java Bytecode
- Title（参考訳）: Petrify: Petri-netによるJavaバイトコードの並行性の解析
- Abstract要約: PetrifyがJavaバイトコードプログラムをペトリネットにエンコード
PNはプログラムの同時動作のかなり正確な符号化である。
Petrifyは、Javaのどのバージョンでも書かれたプログラムや、Kotlinのサブセットにも適用できます。
- 参考スコア（独自算出の注目度）: 1.6901808995670526
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The landscape of automated formal verification is populated by techniques that make prominently different trade-offs: some focus on expressiveness and precision, supporting the verification of complex properties; others favor scalability and practicality, so that they are applicable to larger programs using different features. This paper presents Petrify, a novel automated verification technique for concurrency properties that achieves a distinctive trade-off. Petrify encodes the semantics of Java bytecode programs into Petri nets (PNs), which can be analyzed by state-of-the-art model checking tools such as LoLA. As our experiments demonstrate, Petrify's approach offers an interesting combination of expressiveness and practicality: PNs are a fairly precise encoding of the concurrent behavior of programs; at the same time, Petrify's PN encoding is succinct, so that its analysis remains quite insensitive to parameter size. Another practical benefit of targeting bytecode is that jPetrify, the prototype tool that implements the Petrify technique, is applicable to programs written in any version of Java and even a subset of Kotlin (another language that compiles to Java bytecode) while other similar tools are limited to older versions of Java. While this paper's experiments focus on analyzing fundamental properties like deadlock, Petrify's approach lends itself to be extended to other kinds of concurrency analysis, which we plan to tackle in future work.
- Abstract（参考訳）: 自動形式検証の背景には、表現力と精度を重視し、複雑な性質の検証をサポートする技術や、スケーラビリティと実用性を重視し、異なる特徴を持つ大規模プログラムに適用できる技術がある。
本稿では,並列性に関する新たな自動検証手法であるPetifyについて述べる。
PetrifyはJavaバイトコードプログラムのセマンティクスをPetrinet(PN)にエンコードする。
PNはプログラムの同時動作のかなり正確な符号化であり、同時に、PetifyのPNエンコーディングは簡潔であり、その解析はパラメータサイズにかなり敏感である。
Petrifyテクニックを実装したプロトタイプツールであるjPetrifyは、Javaのあらゆるバージョンで書かれたプログラムや、Kotlin(Javaバイトコードにコンパイルされる他の言語)のサブセットにも適用できます。
本稿では,デッドロックなどの基本特性の分析に焦点をあてるが,Petifyのアプローチは,今後の作業で取り組む予定の,他の種類の並行解析にまで拡張される。
関連論文リスト
- Technical Report: A Formal Semantics for Java Symbolic Evaluation using Large-Block Encoding [0.9985222473972001]
シンボリック実行はバグを見つけ、テストケースを生成し、正確性を保証するために使用される。
Java Rangerは、命令型Javaコードを形式論理の言語に段階的に変換するJavaプログラムのためのパスマージツールである。
これらの変換を形式化し、Javaの具体的セマンティクスの簡易バージョンに関して、それらの健全性を証明します。
論文 参考訳（メタデータ） (2026-08-05T06:49:28Z) - Is Code Better Than Language for Algorithmic Reasoning [58.86873062890482]
ツール拡張言語モデルでは、中間表現と実行機構の両方を変えるため、自然言語推論とコード実行パイプラインを比較することは困難である。
モデルは、その推論を実行可能なコードとして表現し、言語モデルは、そのコードを文脈でシミュレートして、回答を生成する。
中間介入は自然言語の推論と有意に異なるものではない(+0.15pp)。
論文 参考訳（メタデータ） (2026-06-14T04:17:21Z) - How Different Tokenization Algorithms Impact LLMs and Transformer Models for Binary Code Analysis [0.0]
その重要性にもかかわらず、アセンブリコードのコンテキストにおけるトークン化は未探索領域のままである。
我々は、アセンブリコードのユニークな特徴に合わせて、プリプロセスのカスタマイズオプションとプリトークン化ルールについて検討する。
我々は,トークン化効率,語彙圧縮,組立符号の表現忠実度に基づくトークン化器の比較を行った。
論文 参考訳（メタデータ） (2025-11-05T19:45:26Z) - Alignment with Fill-In-the-Middle for Enhancing Code Generation [56.791415642365415]
コードスニペットを小さな粒度のブロックに分割し,同じテストケースからより多様なDPOペアを生成する手法を提案する。
提案手法は,HumanEval (+), MBPP (+), APPS, LiveCodeBench, BigCodeBenchといったベンチマークデータセットの実験によって検証された,コード生成タスクの大幅な改善を示す。
論文 参考訳（メタデータ） (2025-08-27T03:15:53Z) - Parallel Decoding via Hidden Transfer for Lossless Large Language Model Acceleration [54.897493351694195]
本稿では,複数連続するトークンを1つのフォワードパスで同時に復号する,新しい並列復号法,すなわちthithidden Transferを提案する。
加速度測定では,Medusa や Self-Speculative decoding など,単モデル加速技術よりも優れています。
論文 参考訳（メタデータ） (2024-04-18T09:17:06Z) - Extended Paper: API-driven Program Synthesis for Testing Static Typing
Implementations [11.300829269111627]
本稿では,API駆動型プログラム合成の概念に基づいて静的型付けの実装をテストする新しい手法を提案する。
このアイデアは、既存のソフトウェアライブラリから派生したアプリケーションプログラミングインタフェース(API)を活用して組み合わせることで、型集約型だが小さく、十分に型付けされたプログラムを合成することである。
論文 参考訳（メタデータ） (2023-11-08T08:32:40Z) - Learning Type Inference for Enhanced Dataflow Analysis [6.999203506253375]
我々は、型アノテーションを確実に予測するように訓練されたTransformerベースのモデルであるCodeTIDAL5を提案する。
私たちのモデルは、MaryTypes4TypeScriptベンチマークで現在の最先端を7.85%上回っています。
JoernTIは、オープンソースの静的解析ツールであるJoernへの私たちのアプローチの統合です。
論文 参考訳（メタデータ） (2023-10-01T13:52:28Z) - TypeT5: Seq2seq Type Inference using Static Analysis [51.153089609654174]
本稿では,型予測をコード入力タスクとして扱う新しい型推論手法を提案する。
本手法では静的解析を用いて,型シグネチャがモデルによって予測されるコード要素毎に動的コンテキストを構築する。
また,モデルの入力コンテキストに事前の型予測を組み込んだ反復復号方式を提案する。
論文 参考訳（メタデータ） (2023-03-16T23:48:00Z) - DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice [8.735998284944436]
我々はこの検証問題の理論と実践に貢献する。
静的同値、トレース同値およびラベル付き二相性のための新しい複雑性結果を確立する。
我々の手順は、多種多様な暗号プリミティブに対して、トレース同値とラベル付き二相性を決定する最初の方法である。
論文 参考訳（メタデータ） (2022-11-06T22:01:04Z) - Exploring Software Naturalness through Neural Language Models [56.1315223210742]
ソフトウェア自然性仮説(Software Naturalness hypothesis)は、自然言語処理で使用されるのと同じ手法でプログラミング言語を理解することができると主張している。
この仮説は,事前学習されたトランスフォーマーベース言語モデルを用いて,コード解析タスクを実行することによって検討する。
論文 参考訳（メタデータ） (2020-06-22T21:56:14Z) - A Transformer-based Approach for Source Code Summarization [86.08359401867577]
コードトークン間のペア関係をモデル化することにより,要約のためのコード表現を学習する。
アプローチは単純であるにもかかわらず、最先端技術よりもかなりの差があることが示される。
論文 参考訳（メタデータ） (2020-05-01T23:29:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。