Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911928858705920 |
|---|---|
| author | Menezes, Rafael Sá Manino, Edoardo Shmarov, Fedor Aldughaim, Mohannad de Freitas, Rosiane Cordeiro, Lucas C. |
| author_facet | Menezes, Rafael Sá Manino, Edoardo Shmarov, Fedor Aldughaim, Mohannad de Freitas, Rosiane Cordeiro, Lucas C. |
| contents | Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use. In more detail, we quantify the benefits of interval analysis on two benchmarks: the Intel Core Power Management firmware and 9537 programs in the ReachSafety category of the International Competition on Software Verification. Our results show that interval analysis is essential in solving 203 unique benchmarks. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_15281 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study Menezes, Rafael Sá Manino, Edoardo Shmarov, Fedor Aldughaim, Mohannad de Freitas, Rosiane Cordeiro, Lucas C. Software Engineering Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use. In more detail, we quantify the benefits of interval analysis on two benchmarks: the Intel Core Power Management firmware and 9537 programs in the ReachSafety category of the International Competition on Software Verification. Our results show that interval analysis is essential in solving 203 unique benchmarks. |
| title | Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2406.15281 |