一句话：提出模型检测器 IDPVerifier，在约束编码阶段利用中断语义与启发式、约简偏序约束，加速中断驱动程序的断言违例检测。
中断驱动程序广泛用于安全关键系统，但优先级任务的非确定性交错常引发并发缺陷，现有工具在断言违例检测上难以兼顾精度与效率。本文提出一种模型检测方法，在约束编码阶段利用中断机制剪枝搜索空间：以精确偏序约束刻画任务交错，用基于并发控制关系的启发式约束引导求解器，并借助中断的 enable-before 机制识别并剔除不可行偏序约束，从而得到更易求解的简化公式。作者将该方法实现为模型检测器 IDPVerifier，在 24 个真实基准上评测，表明该策略在保持高精度的同时显著缩短求解时间，并优于当前最优基线。
Interrupt-driven programs are widely used in safety-critical systems, but non-deterministic interleavings of prioritized tasks often lead to concurrency defects. While assertion violation detection is essential for program correctness, achieving precision and efficiency remains challenging for current tools. To address this issue, we propose a model checking approach that leverages interrupt mechanisms to prune the search space at the constraint-encoding stage. Specifically, precise partial-order constraints represent task interleavings, while heuristic constraints based on concurrency-control relations guide the solver. Furthermore, by considering the enable-before mechanism in interrupts, infeasible partial-order constraints are identified and eliminated, resulting in simplified formulas for efficient reasoning. Our approach has been implemented in a model checker namely IDPVerifier. Evaluation across 24 real-world benchmarks demonstrates that our strategies significantly reduce solving time while maintaining high accuracy, outperforming state-of-the-art baselines. This work shows how leveraging interrupt semantics in constraint encoding can mitigate the state-space explosion in verifying complex embedded software.
@inproceedings{YuanYLWLWWC26,
title = {IDPVerifier: Verifying Interrupt-driven Programs Efficiently via Heuristic and Reduced Partial-order Constraints},
author = {Zixuan Yuan and Bin Yu and Xu Lu and Wensheng Wang and Yuanzhe Liu and Cheng Wen and Meng Wang and Chu Chen},
booktitle = {FSE},
year = {2026},
doi = {10.1145/3803437.3805563}
}