Navegar

Colección

Datos Estadísticas

Conferencia

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" (2017) 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017:200-205
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor

Abstract:

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.

Registro:

Documento: Conferencia
Título:Model checker execution reports
Autor: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
Filiación:Departamento de Computación, FCEyN, UBA, CONICET, Buenos Aires, Argentina
Palabras clave:Software engineering; Abstract reachability trees; Model checker; Software model checkers; Software model checking; Model checking
Año:2017
Página de inicio:200
Página de fin:205
DOI: http://dx.doi.org/10.1109/ASE.2017.8115633
Título revista:32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017
Título revista abreviado:ASE - Proc. IEEE/ACM Int. Conf. Autom. Softw. Eng.
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97815386_v_n_p200_Castano

Referencias:

  • Ball, T., Levin, V., Rajamani, S.K., A decade of software model checking with slam (2011) Communications of the ACM, 54 (7), pp. 68-76
  • Beyer, D., Software verification and verifiable witnesses (2015) Tools and Algorithms for the Construction and Analysis of Systems, pp. 401-416. , Springer
  • Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A., Witness validation and stepwise testification across software verifiers (2015) Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 721-733. , ACM
  • Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P., (2011) Conditional Model Checking, , arXiv preprint arXiv:1109.6926
  • Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P., Conditional model checking: A technique to pass information between verifiers (2012) Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, p. 57. , ACM
  • Beyer, D., Henzinger, T.A., Théoduloz, G., Configurable software verification: Concretizing the convergence of model checking and program analysis (2007) Computer Aided Verification, pp. 504-518. , Springer
  • Beyer, D., Löwe, S., Explicit-state software model checking based on cegar and interpolation (2013) International Conference on Fundamental Approaches to Software Engineering, pp. 146-162. , Springer
  • Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y., Symbolic model checking using sat procedures instead of bdds (1999) Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, pp. 317-320. , ACM
  • Cadar, C., Sen, K., Symbolic execution for software testing: Three decades later (2013) Communications of the ACM, 56 (2), pp. 82-90
  • Castaño, R., Braberman, V., Garbervetsky, D., Uchitel, S., (2016) Model Checker Execution Reports, , arXiv preprint arXiv:1607.06857
  • Christakis, M., Leino, K.R.M., Müller, P., Wüstholz, V., Integrated environment for diagnosing verification errors (2016) International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 424-441. , Springer
  • Christakis, M., Müller, P., Wüstholz, V., Collaborative verification and testing with explicit assumptions (2012) FM 2012: Formal Methods, pp. 132-146. , Springer
  • Czech, M., Jakobs, M.-C., Wehrheim, H., Just test what you cannot verify (2015) Fundamental Approaches to Software Engineering, pp. 100-114. , Springer
  • D'Ippolito, N., Frias, M.F., Galeotti, J.P., Lanzarotti, E., Mera, S., Alloy+ hotcore: A fast approximation to unsat core (2010) Abstract State Machines, Alloy, B and Z, pp. 160-173. , Springer
  • Filieri, A., Pasareanu, C.S., Visser, W., Reliability analysis in symbolic pathfinder (2013) Proceedings of the 2013 International Conference on Software Engineering, pp. 622-631. , IEEE Press
  • Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G., Lazy abstraction (2002) ACM SIGPLAN Notices, 37 (1), pp. 58-70
  • Jackson, D., (2012) Software Abstractions: Logic, Language, and Analysis, , MIT press
  • Jhala, R., Majumdar, R., Software model checking (2009) ACM Computing Surveys (CSUR), 41 (4), p. 21
  • Lal, A., Qadeer, S., Powering the static driver verifier using corral (2014) Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 202-212. , ACM
  • Lal, A., Qadeer, S., Lahiri, S.K., A solver for reachability modulo theories (2012) International Conference on Computer Aided Verification, pp. 427-443. , Springer
  • Leino, K.R.M., Dafny: An automatic program verifier for functional correctness (2010) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348-370. , Springer
  • Pavese, E., Braberman, V., Uchitel, S., My model checker died!: How well did it do? (2010) Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems, pp. 33-40. , ACM
  • Tulsian, V., Kanade, A., Kumar, R., Lal, A., Nori, A.V., Mux: Algorithm selection for software model checkers (2014) Proceedings of the 11th Working Conference on Mining Software Repositories, pp. 132-141. , ACMA4 - College of Engineering; Denso; et al.; Microsoft; NASA; University of Minnesota, Software Engineering

Citas:

---------- APA ----------
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 (2017) . Model checker execution reports. 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, 200-205.
http://dx.doi.org/10.1109/ASE.2017.8115633
---------- CHICAGO ----------
Castano, R., Braberman, V., Garbervetsky, D., Uchitel, S., Nguyen T.N., Rosu G., et al. "Model checker execution reports" . 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017 (2017) : 200-205.
http://dx.doi.org/10.1109/ASE.2017.8115633
---------- MLA ----------
Castano, R., Braberman, V., Garbervetsky, D., Uchitel, S., Nguyen T.N., Rosu G., et al. "Model checker execution reports" . 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, 2017, pp. 200-205.
http://dx.doi.org/10.1109/ASE.2017.8115633
---------- VANCOUVER ----------
Castano, R., Braberman, V., Garbervetsky, D., Uchitel, S., Nguyen T.N., Rosu G., et al. Model checker execution reports. ASE - Proc. IEEE/ACM Int. Conf. Autom. Softw. Eng. 2017:200-205.
http://dx.doi.org/10.1109/ASE.2017.8115633