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...

Descripción completa

Detalles Bibliográficos
Autores principales:	Castano, R., Braberman, V., Garbervetsky, D., Uchitel, S., Nguyen T.N., Rosu G., Di Penta M., College of Engineering; Denso; et al.; Microsoft; NASA; University of Minnesota, Software Engineering
Formato:	CONF
Materias:	Software engineering Abstract reachability trees Model checker Software model checkers Software model checking Model checking
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_97815386_v_n_p200_Castano
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_97815386_v_n_p200_Castano
record_format	dspace
spelling	todo:paper_97815386_v_n_p200_Castano2023-10-03T16:43:53Z Model checker execution reports Castano, R. Braberman, V. Garbervetsky, D. Uchitel, S. Nguyen T.N. Rosu G. Di Penta M. College of Engineering; Denso; et al.; Microsoft; NASA; University of Minnesota, Software Engineering 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. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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 Castano, R. Braberman, V. Garbervetsky, D. Uchitel, S. Nguyen T.N. Rosu G. Di Penta M. College of Engineering; Denso; et al.; Microsoft; NASA; University of Minnesota, Software Engineering 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.
format	CONF
author	Castano, R. Braberman, V. Garbervetsky, D. Uchitel, S. Nguyen T.N. Rosu G. Di Penta M. College of Engineering; Denso; et al.; Microsoft; NASA; University of Minnesota, Software Engineering
author_facet	Castano, R. Braberman, V. Garbervetsky, D. Uchitel, S. Nguyen T.N. Rosu G. Di Penta M. College of Engineering; Denso; et al.; Microsoft; NASA; University of Minnesota, Software Engineering
author_sort	Castano, R.
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
url	http://hdl.handle.net/20.500.12110/paper_97815386_v_n_p200_Castano
work_keys_str_mv	AT castanor modelcheckerexecutionreports AT brabermanv modelcheckerexecutionreports AT garbervetskyd modelcheckerexecutionreports AT uchitels modelcheckerexecutionreports AT nguyentn modelcheckerexecutionreports AT rosug modelcheckerexecutionreports AT dipentam modelcheckerexecutionreports AT collegeofengineeringdensoetalmicrosoftnasauniversityofminnesotasoftwareengineering modelcheckerexecutionreports
_version_	1807322245311234048

Model checker execution reports

Ejemplares similares