A shallow dive into the depths of non-termination checking for C programs
<|reference_start|>A shallow dive into the depths of non-termination checking for C programs: Checking for Non-Termination (NT) of a given program P, i.e., determining if P has at least one non-terminating run, is an undecidable problem that continues to garner significant research attention. While unintended NT is common in real-world software development, even the best-performing tools for NT checking are often ineffective on real-world programs and sometimes incorrect due to unrealistic assumptions such as absence of overflows. To address this, we propose a sound and efficient technique for NT checking that is also effective on realworld software. Given P, we encode the NT property as an assertion inside each loop of P to check for recurrent states in that loop, up to a fixed unwinding depth, using a Bounded Model Checker. The unwinding depth is increased iteratively until either NT is found or a predefined limit is reached. Our experiments on wide ranging software benchmarks show that the technique outperforms state-of-the-art NT checkers<|reference_end|>
@article{metta2024a,
    title={A shallow dive into the depths of non-termination checking for C
  programs},
    author={Ravindra Metta, Hrishikesh Karmarkar, Kumar Madhukar, R Venkatesh,
  Supratik Chakraborty, Samarjit Chakraborty},
    journal={arXiv preprint arXiv:2409.12985},
    year={2024},
    archivePrefix={arXiv},
    eprint={2409.12985},
    primaryClass={cs.SE cs.LO}
}