A shallow dive into the depths of non-termination checking for C programs
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914953330425856 |
|---|---|
| author | Metta, Ravindra Karmarkar, Hrishikesh Madhukar, Kumar Venkatesh, R Chakraborty, Supratik Chakraborty, Samarjit |
| author_facet | Metta, Ravindra Karmarkar, Hrishikesh Madhukar, Kumar Venkatesh, R Chakraborty, Supratik Chakraborty, Samarjit |
| contents | 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 |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_12985 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A shallow dive into the depths of non-termination checking for C programs Metta, Ravindra Karmarkar, Hrishikesh Madhukar, Kumar Venkatesh, R Chakraborty, Supratik Chakraborty, Samarjit Software Engineering Logic in Computer Science 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 |
| title | A shallow dive into the depths of non-termination checking for C programs |
| topic | Software Engineering Logic in Computer Science |
| url | https://arxiv.org/abs/2409.12985 |