PSR2: A Phase-based Semantic Reasoning Framework for Atomicity Violation Detection via Contract Refinement

• URL: http://arxiv.org/abs/2604.06975v2
• Date: Mon, 13 Apr 2026 11:05:43 GMT
• Title: PSR2: A Phase-based Semantic Reasoning Framework for Atomicity Violation Detection via Contract Refinement
• Abstract summary: PSRtextsuperscript2 is a novel collaborative static analysis framework that integrates structural path searching with deterministic semantic reasoning.<n>Experiments on 1,600 contract samples demonstrate that PSRtextsuperscript2 significantly outperforms pattern-matching baselines.<n>Our fusion logic effectively reduces the false-positive rate by nearly half compared to single module analysis.
• Score: 9.36682660657815
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: With the rapid advancement of decentralized applications, smart contract security faces severe challenges, particularly regarding atomicity violations in complex logic such as Oracle and NFT contracts. Rigid rule sets often limit traditional static analyzers and lack deep contextual awareness, leading to high false-positive and false-negative rates when identifying vulnerabilities that depend on intermediate state inconsistencies. To address these limitations, this paper proposes PSR\textsuperscript{2}, a novel collaborative static analysis framework that integrates structural path searching with deterministic semantic reasoning. PSR\textsuperscript{2} utilizes a Graph Structure Analysis Module (GSAM) to identify suspicious execution sequences in control flow graphs and a Semantic Context Analysis Module (SCAM) to extract data dependencies and state facts from abstract syntax trees. A Fusion Decision Module (FDM) then performs formal cross validation to confirm vulnerabilities based on a unified atomicity inconsistency model. Experimental results on 1,600 contract samples demonstrate that PSR\textsuperscript{2} significantly outperforms pattern-matching baselines, achieving an F1-score of 94.69\% in complex ERC-721 scenarios compared to 51.86\% for existing tools. Ablation studies further confirm that our fusion logic effectively reduces the false-positive rate by nearly half compared to single module analysis.

Related papers

• Neuro-symbolic PRM: Enhancing Scientific Reasoning via Structured Traces and Symbolic Verification [10.892972402027494]
  Intermediate reasoning steps are syntactically well-formed, mathematically executable, and unit-consistent, yet contextually ungrounded.<n>Current approaches either rely on formal verifiers that cannot assess semantic intent, or burden Process Reward Models (PRMs) with the dual task of checking both arithmetic and logic.<n>We propose a neuro-symbolic framework that cleanly decouples reasoning into two formal dimensions: Symbolic Validity ($V$) and Semantic Groundedness ($G$)
  arXiv  Detail & Related papers  (2026-08-26T19:10:12Z)
• A Temporal Reasoning Benchmarking Framework for LRMs via Difficulty-controlled and Dynamic Test Generation [11.290047096794082]
  We introduce TRACE, a testing framework that models temporal reasoning as constraint satisfaction problems via Allen's Interval Algebra.<n>TRACE provides a robust, automated platform for benchmarking the true temporal reasoning capabilities of LRMs.
  arXiv  Detail & Related papers  (2026-07-06T08:14:53Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Auto-ART: Structured Literature Synthesis and Automated Adversarial Robustness Testing [0.0]
  We analyze nine peer-reviewed corpus sources through seven complementary protocols.<n>We introduce Auto-ART, an open-source framework that operationalizes identified gaps.<n> Empirical validation on RobustBench demonstrates that Auto-ART's pre-screening identifies gradient masking in 92% of flagged cases.
  arXiv  Detail & Related papers  (2026-04-22T15:46:11Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• Sharp Convergence Rates for Masked Diffusion Models [53.117058231393834]
  We develop a total-variation based analysis for the Euler method that overcomes limitations.<n>Our results relax assumptions on score estimation, improve parameter dependencies, and establish convergence guarantees.<n>Overall, our analysis introduces a direct TV-based error decomposition along the CTMC trajectory and a decoupling-based path-wise analysis for FHS.
  arXiv  Detail & Related papers  (2026-02-26T00:47:51Z)
• Diagnosing Structural Failures in LLM-Based Evidence Extraction for Meta-Analysis [0.8193467416247519]
  Review and meta-analyses rely on converting narrative articles into structured, numerically grounded study records.<n>Despite rapid advances in large language models (LLMs), it remains unclear whether they can meet the structural requirements of this process.<n>We propose a structural, diagnostic framework that evaluates LLM-based evidence extraction as a progression of schema-constrained queries.
  arXiv  Detail & Related papers  (2026-02-11T14:09:43Z)
• CoG: Controllable Graph Reasoning via Relational Blueprints and Failure-Aware Refinement over Knowledge Graphs [53.199517625701475]
  CoG is a training-free framework inspired by Dual-Process Theory that mimics the interplay between intuition and deliberation.<n>CoG significantly outperforms state-of-the-art approaches in both accuracy and efficiency.
  arXiv  Detail & Related papers  (2026-01-16T07:27:40Z)
• Cracking IoT Security: Can LLMs Outsmart Static Analysis Tools? [1.8549313085249322]
  This work presents the first comprehensive evaluation of Large Language Models (LLMs) across a multi-category interaction threat taxonomy.<n>We benchmark Llama 3.1 8B, Llama 70B, GPT-4o, Gemini-2.5-Pro, and DeepSeek-R1 across zero-, one-, and two-shot settings.<n>Our findings show that while LLMs exhibit promising semantic understanding, their accuracy degrades significantly for threats requiring cross-rule structural reasoning.
  arXiv  Detail & Related papers  (2026-01-02T04:17:36Z)
• KBQA-R1: Reinforcing Large Language Models for Knowledge Base Question Answering [64.62317305868264]
  We present textbfKBQA-R1, a framework that shifts the paradigm from text imitation to interaction optimization via Reinforcement Learning.<n>Treating KBQA as a multi-turn decision process, our model learns to navigate the knowledge base using a list of actions.<n>Experiments on WebQSP, GrailQA, and GraphQuestions demonstrate that KBQA-R1 achieves state-of-the-art performance.
  arXiv  Detail & Related papers  (2025-12-10T17:45:42Z)
• Hierarchical Evaluation of Software Design Capabilities of Large Language Models of Code [7.897548449569687]
  Large language models (LLMs) are increasingly adopted in software engineering domain, yet robustness of their grasp on core design concepts remains unclear.<n>We generate poorly designed software fragments under various levels of guidance.<n> Reasoning about coupling proves brittle; performance collapses in noisy, open-ended scenarios.<n> Reasoning-trace analysis confirms these failure modes, revealing textitcognitive shortcutting for coupling versus a more exhaustive (yet still failing) analysis for cohesion.
  arXiv  Detail & Related papers  (2025-11-25T23:50:00Z)
• From Harm to Help: Turning Reasoning In-Context Demos into Assets for Reasoning LMs [58.02809208460186]
  We revisit this paradox using high-quality traces from DeepSeek-R1 as demonstrations.<n>We find that adding more exemplars consistently degrades accuracy, even when demonstrations are optimal.<n>We introduce Insight-to-solve (I2S), a sequential test-time procedure that turns demonstrations into explicit, reusable insights.
  arXiv  Detail & Related papers  (2025-09-27T08:59:31Z)
• VulAgent: Hypothesis-Validation based Multi-Agent Vulnerability Detection [55.957275374847484]
  VulAgent is a multi-agent vulnerability detection framework based on hypothesis validation.<n>It implements a semantics-sensitive, multi-view detection pipeline, each aligned to a specific analysis perspective.<n>On average, VulAgent improves overall accuracy by 6.6%, increases the correct identification rate of vulnerable--fixed code pairs by up to 450%, and reduces the false positive rate by about 36%.
  arXiv  Detail & Related papers  (2025-09-15T02:25:38Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.