Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement

• URL: http://arxiv.org/abs/2509.13699v1
• Date: Wed, 17 Sep 2025 05:05:16 GMT
• Title: Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
• Authors: Max Barth, Marie-Christine Jakobs,
• Abstract summary: We propose a solution to parallelize trace abstraction, an abstraction-based approach to software model checking.<n>Our approach is more effective than DSS, a recent parallel approach to abstraction-based software model checking.
• Score: 1.955166888058497
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automatic software verification is a valuable means for software quality assurance. However, automatic verification and in particular software model checking can be time-consuming, which hinders their practical applicability e.g., the use in continuous integration. One solution to address the issue is to reduce the response time of the verification procedure by leveraging today's multi-core CPUs. In this paper, we propose a solution to parallelize trace abstraction, an abstraction-based approach to software model checking. The underlying idea of our approach is to parallelize the abstraction refinement. More concretely, our approach analyzes different traces (syntactic program paths) that could violate the safety property in parallel. We realize our parallelized version of trace abstraction in the verification tool Ulti mate Automizer and perform a thorough evaluation. Our evaluation shows that our parallelization is more effective than sequential trace abstraction and can provide results significantly faster on many time-consuming tasks. Also, our approach is more effective than DSS, a recent parallel approach to abstraction-based software model checking.

Related papers

• Detecting Object Tracking Failure via Sequential Hypothesis Testing [80.7891291021747]
  Real-time online object tracking in videos constitutes a core task in computer vision.<n>We propose interpreting object tracking as a sequential hypothesis test, wherein evidence for or against tracking failures is gradually accumulated over time.<n>We propose both supervised and unsupervised variants by leveraging either ground-truth or solely internal tracking information.
  arXiv  Detail & Related papers  (2026-02-13T14:57:15Z)
• Learning to Share: Selective Memory for Efficient Parallel Agentic Systems [49.78267008828593]
  Agentic systems solve complex tasks by coordinating multiple agents that iteratively reason, invoke tools, and exchange intermediate results.<n>Recent approaches deploy multiple agent teams running in parallel to explore diverse reasoning trajectories.<n>We propose Learning to Share (LTS), a learned shared-memory mechanism for parallel agentic frameworks.
  arXiv  Detail & Related papers  (2026-02-05T18:20:21Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  Inference-time compute has re-emerged as a practical way to improve LLM reasoning.<n>Most test-time scaling (TTS) algorithms rely on autoregressive decoding.<n>We propose Prism, an efficient TTS framework for dLLMs.
  arXiv  Detail & Related papers  (2026-02-02T09:14:51Z)
• Learning Latency-Aware Orchestration for Parallel Multi-Agent Systems [18.192867631682674]
  We investigate learning-based orchestration of multi-agent systems with explicit latency under parallel execution.<n>We propose latency-aware Multi-agent System (LAMaS), a work-aware multi-agent orchestration framework.<n>Our experiments show that our approach reduces critical path length by 38-46% compared to the state-of-the-art baseline for multi-agent architecture search.
  arXiv  Detail & Related papers  (2026-01-15T16:23:53Z)
• dParallel: Learnable Parallel Decoding for dLLMs [77.24184219948337]
  Diffusion large language models (dLLMs) offer parallel token prediction and lower inference latency.<n>Existing open-source models still require nearly token-length decoding steps to ensure performance.<n>We introduce dParallel, a simple and effective method that unlocks the inherent parallelism of dLLMs for fast sampling.
  arXiv  Detail & Related papers  (2025-09-30T16:32:52Z)
• SPARE: Single-Pass Annotation with Reference-Guided Evaluation for Automatic Process Supervision and Reward Modelling [58.05959902776133]
  We introduce Single-Pass.<n>with Reference-Guided Evaluation (SPARE), a novel structured framework that enables efficient per-step annotation.<n>We demonstrate SPARE's effectiveness across four diverse datasets spanning mathematical reasoning (GSM8K, MATH), multi-hop question answering (MuSiQue-Ans), and spatial reasoning (SpaRP)<n>On ProcessBench, SPARE demonstrates data-efficient out-of-distribution generalization, using only $sim$16% of training samples compared to human-labeled and other synthetically trained baselines.
  arXiv  Detail & Related papers  (2025-06-18T14:37:59Z)
• Structural Abstraction and Selective Refinement for Formal Verification [0.5735035463793008]
  Safety verification of robot applications is extremely challenging due to the complexity of the environment that a robot typically operates in.<n>A usual solution approach is abstraction, more precisely behavioral abstraction.<n>We propose structural abstraction instead, which we investigated in the context of voxel representation of the robot environment.
  arXiv  Detail & Related papers  (2025-05-29T01:44:47Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  We propose a unified Test-Time Compute scaling framework that leverages increased inference-time instead of larger models.<n>Our framework incorporates two complementary strategies: internal TTC and external TTC.<n>We demonstrate our textbf32B model achieves a 46% issue resolution rate, surpassing significantly larger models such as DeepSeek R1 671B and OpenAI o1.
  arXiv  Detail & Related papers  (2025-03-31T07:31:32Z)
• A Case Study on Model Checking and Runtime Verification for Awkernel [0.7199733380797578]
  It is difficult for humans to manually review concurrent behaviors or to write test cases covering all possible executions.<n>This paper proposes a development method for concurrent software, such as schedulers.
  arXiv  Detail & Related papers  (2025-03-12T11:27:45Z)
• Code Review Automation Via Multi-task Federated LLM -- An Empirical Study [4.8342038441006805]
  The study explores five simple techniques for multi-task training, including two sequential methods, one parallel method, and two cumulative methods.<n>The results indicate that sequentially training a federated LLM (FedLLM) for our code review multi-task use case is less efficient in terms of time, computation, and performance metrics, compared to training separate models for each task.
  arXiv  Detail & Related papers  (2024-12-20T08:46:46Z)
• Step-by-Step Reasoning for Math Problems via Twisted Sequential Monte Carlo [55.452453947359736]
  We introduce a novel verification method based on Twisted Sequential Monte Carlo (TSMC)<n>We apply TSMC to Large Language Models by estimating the expected future rewards at partial solutions.<n>This approach results in a more straightforward training target that eliminates the need for step-wise human annotations.
  arXiv  Detail & Related papers  (2024-10-02T18:17:54Z)
• Transformer-based assignment decision network for multiple object tracking [2.2920634931825803]
  We introduce Transformer-based Assignment Decision Network (TADN) that tackles data association without the need of explicit optimization during inference.<n>Our proposed approach demonstrates strong performance in most evaluation metrics despite its simple nature as a tracker.
  arXiv  Detail & Related papers  (2022-08-06T19:47:32Z)
• Parallel and Multi-Objective Falsification with Scenic and VerifAI [11.152087017964584]
  We present extensions to the Scenic scenario specification language and VerifAI toolkit. We first present a parallelized framework that is interfaced with both the simulation and sampling capabilities of Scenic. We then present an extension of VerifAI's falsification algorithms to support multi-objective optimization during sampling.
  arXiv  Detail & Related papers  (2021-07-09T01:08:49Z)

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.