arXiv 1509.024902015-09-08cs.LOcs.SE

Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)

Erickson H. da S. Alves, Lucas C. Cordeiro, Eddie B. de Lima Filho

备注：: extended version of paper published at SBESC'15

英文摘要：

Software debugging is a very time-consuming process, which is even worse for multi-threaded programs, due to the non-deterministic behavior of thread-scheduling algorithms. However, the debugging time may be greatly reduced, if automatic methods are used for localizing faults. In this study, a new method for fault localization, in multi-threaded C programs, is proposed. It transforms a multi-threaded program into a corresponding sequential one and then uses a fault-diagnosis method suitable for this type of program, in order to localize faults. The code transformation is implemented with rules and context switch information from counterexamples, which are typically generated by bounded model checkers. Experimental results show that the proposed method is effective, in such a way that sequential fault-localization methods can be extended to multi-threaded programs.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Bounded Model Checking of Multi-threaded Software using SMT solvers

The transition from single-core to multi-core processors has made multi-threaded software an important subject in computer aided verification. Here, we describe and evaluate an extension of the ESBMC model checker to support the verification of multi-threaded software with shared variables and locks using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT). We describe three approaches to model check multi-threaded software and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the…

2010-03-19cs.LOcs.SE

通过并行轨迹抽象细化实现多线程软件模型检查

Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement

本文提出了一种基于并行轨迹抽象细化的多线程软件模型检查方法，通过利用多核CPU提升验证效率，优于传统顺序方法和DSS技术。

2026-01-15cs.LOcs.PLcs.SE

LTL Model-Checking for Dynamic Pushdown Networks Communicating via Locks

A Dynamic Pushdown Network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded programs with (possibly recursive) procedure calls and thread creation. Extending DPNs with locks allows processes to synchronize with each other. Thus, DPNs with locks are a well adapted formalism to model multi-threaded programs that synchronize via locks. Therefore, it is important to have model-checking algorithms for DPNs with locks. We consider in this work model-checking for DPNs with locks against single-indexed…

2016-10-11cs.LOcs.PLcs.SE

Dynamic Fault Trees Analysis using an Integration of Theorem Proving and Model Checking

Dynamic fault trees (DFTs) have emerged as an important tool for capturing the dynamic behavior of system failure. These DFTs are then analyzed qualitatively and quantitatively using stochastic or algebraic methods to judge the failure characteristics of the given system in terms of the failures of its sub-components. Model checking has been recently proposed to conduct the failure analysis of systems using DFTs with the motivation to provide a rigorous failure analysis of safety-critical systems. However, model checking has not been used for the DFT qualitative analysis and the reduction algo…

2017-12-07cs.LO

Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar

Model checking of real-time systems has evolved throughout the years. Recently, the model checker Ecdar, using timed I/O automata, was used to perform compositional verification. However, in order to fully integrate model checking of real-time systems into industrial development, we need a productive and reliable way to test if such a system conforms to its corresponding model. Hence, we present an extension of Ecdar that integrates conformance testing into a new IDE that now features modelling, verification, and testing. The new tool uses model-based mutation testing, requiring only the model…

2018-09-10cs.LOcs.SE

Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms

We introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA). FTDAs are parameterized by both the number of processes and the assumed maximum number of Byzantine faulty processes. At the center of our technique is a parametric interval abstraction (PIA) where the interval boundaries are arithmetic expressions over parameters. Using PIA for both data abstraction and a new form of counter abstraction, we reduce the parameterized problem to finite-state model checking. We demonstrate the practical feasibility of our method by verifying several varia…

2013-02-03cs.DCcs.LO

更多相关论文收起更多论文

基于故障维护树的智能建筑维护高效概率模型检查

Efficient Probabilistic Model Checking of Smart Building Maintenance using Fault Maintenance Trees

University of Oxford（牛津大学）；University of Twente（特温特大学）

本文提出利用概率模型检查构建故障维护树框架，通过抽象算法减少连续时间马尔可夫链规模，提升智能建筑HVAC系统可靠性评估效率。

2018-01-12cs.LOcs.SYeess.SY

A Note on Fault Diagnosis Algorithms

In this paper we review algorithms for checking diagnosability of discrete-event systems and timed automata. We point out that the diagnosability problems in both cases reduce to the emptiness problem for (timed) Büchi automata. Moreover, it is known that, checking whether a discrete-event system is diagnosable, can also be reduced to checking bounded diagnosability. We establish a similar result for timed automata. We also provide a synthesis of the complexity results for the different fault diagnosis problems.

2010-04-16cs.FLcs.LO

探测器错误模型的拟线性等价性检查

Quasilinear Equivalence Checking for Detector Error Models

Unitary Foundation（Unitary基金会）

提出探测器错误模型（DEM）的等式理论，通过拟线性时间归约系统实现结构等价性判定，并应用于量子编译器验证与优化。

2026-06-15cs.LOcs.PLcs.SE

Tarmo: A Framework for Parallelized Bounded Model Checking

This paper investigates approaches to parallelizing Bounded Model Checking (BMC) for shared memory environments as well as for clusters of workstations. We present a generic framework for parallelized BMC named Tarmo. Our framework can be used with any incremental SAT encoding for BMC but for the results in this paper we use only the current state-of-the-art encoding for full PLTL. Using this encoding allows us to check both safety and liveness properties, contrary to an earlier work on distributing BMC that is limited to safety properties only. Despite our focus on BMC after it has been trans…

2009-12-13cs.DCcs.LO

通过区间抽象的有效随机自动机模型检测（扩展版）

Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)

Universidad Nacional de Córdoba（科尔多瓦国立大学）；CONICET（国家科学研究委员会）；University of Twente（特温特大学）

提出一种结合可细化区间抽象与“大时间步”语义的随机自动机模型检测方法，为最大/最小可达概率提供上下界，实验表明对非平凡示例有效。

2026-07-02cs.LO

Debugging Smart Contract's Business Logic Using Symbolic Model-Checking

Smart contracts are a special type of programs running inside a blockchain. Immutable and transparent, they provide means to implement fault-tolerant and censorship-resistant services. Unfortunately, its immutability causes a serious challenge of ensuring that a business logic and implementation is correct upfront, before publishing in a blockchain. Several big accidents have indeed shown that users of this technology need special tools to verify smart contract correctness. Existing automated checkers are able to detect only well known implementation bugs, leaving the question of business logi…

2018-12-03cs.CRcs.LOcs.PL