Model checker execution reports
Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to...
Guardado en:
| Publicado: |
2017
|
|---|---|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97815386_v_n_p200_Castano http://hdl.handle.net/20.500.12110/paper_97815386_v_n_p200_Castano |
| Aporte de: |
| id |
paper:paper_97815386_v_n_p200_Castano |
|---|---|
| record_format |
dspace |
| spelling |
paper:paper_97815386_v_n_p200_Castano2023-06-08T16:37:59Z Model checker execution reports Software engineering Abstract reachability trees Model checker Software model checkers Software model checking Model checking Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to provide a conceptual framing to extend software model checkers in a way that allows users to access information about incomplete checks. We characterize the information that model checkers themselves can provide, in terms of analyzed traces, i.e. sequences of statements, and safe canes, and present the notion of execution reports (ERs), which we also formalize. We instantiate these concepts for a family of techniques based on Abstract Reachability Trees and implement the approach using the software model checker CPAchecker. We evaluate our approach empirically and provide examples to illustrate the ERs produced and the information that can be extracted. © 2017 IEEE. 2017 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97815386_v_n_p200_Castano http://hdl.handle.net/20.500.12110/paper_97815386_v_n_p200_Castano |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Software engineering Abstract reachability trees Model checker Software model checkers Software model checking Model checking |
| spellingShingle |
Software engineering Abstract reachability trees Model checker Software model checkers Software model checking Model checking Model checker execution reports |
| topic_facet |
Software engineering Abstract reachability trees Model checker Software model checkers Software model checking Model checking |
| description |
Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to provide a conceptual framing to extend software model checkers in a way that allows users to access information about incomplete checks. We characterize the information that model checkers themselves can provide, in terms of analyzed traces, i.e. sequences of statements, and safe canes, and present the notion of execution reports (ERs), which we also formalize. We instantiate these concepts for a family of techniques based on Abstract Reachability Trees and implement the approach using the software model checker CPAchecker. We evaluate our approach empirically and provide examples to illustrate the ERs produced and the information that can be extracted. © 2017 IEEE. |
| title |
Model checker execution reports |
| title_short |
Model checker execution reports |
| title_full |
Model checker execution reports |
| title_fullStr |
Model checker execution reports |
| title_full_unstemmed |
Model checker execution reports |
| title_sort |
model checker execution reports |
| publishDate |
2017 |
| url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97815386_v_n_p200_Castano http://hdl.handle.net/20.500.12110/paper_97815386_v_n_p200_Castano |
| _version_ |
1768541869413761024 |