Detecting atomicity violations effectively in interrupt-driven programs is difficult due to the asymmetric concurrency interleaving of interrupts. Current approaches face two main challenges: (1) A large number of false positives are generated by efficient static analysis techniques. (2) Loops with large or unknown bounds in these programs limit the scalability of the bounded verification techniques. To address these challenges, we present NIChecker, a new bounded verification tool designed to detect atomicity violations in interrupt-driven programs. The key ideas are: (1) Transforming an interrupt-driven program into a bounded sequential C program through lazy sequentialization technique. This sequential program accurately models interrupt masking and nested interrupt execution. (2) Combining a refined loop abstraction technique with our sequentialization to enhance the efficiency of detecting programs with intractable loops. (3) Integrating slicing and an interleaving path reduction technique known as preemption point reduction in NIChecker to shrink the explored state space. We prove the bounded correctness of our translation and discuss the impact of our optimizations. We evaluate NIChecker on 31 academic benchmark programs and 18 real-world interrupt-driven programs. Our results show that NIChecker achieves better precision, a lower false positive rate, and a significant verification speed-up than related state-of-the-art tools.