IDPVerifier: Verifying Interrupt-driven Programs Efficiently via Heuristic and Reduced Partial-order Constraints
TL;DR
A model checking approach that leverages interrupt mechanisms to prune the search space at the constraint-encoding stage, showing how leveraging interrupt semantics in constraint encoding can mitigate the state-space explosion in verifying complex embedded software.
Abstract
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.