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:
| Autor principal: | |
|---|---|
| Otros Autores: | , , , , , , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
Institute of Electrical and Electronics Engineers Inc.
2017
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 07714caa a22007097a 4500 | ||
|---|---|---|---|
| 001 | PAPER-17457 | ||
| 003 | AR-BaUEN | ||
| 005 | 20251211113220.0 | ||
| 008 | 190410s2017 xx ||||fo|||| 10| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-85041444655 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Castano, R. | |
| 245 | 1 | 0 | |a Model checker execution reports |
| 260 | |b Institute of Electrical and Electronics Engineers Inc. |c 2017 | ||
| 504 | |a 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 | ||
| 504 | |a Beyer, D., Software verification and verifiable witnesses (2015) Tools and Algorithms for the Construction and Analysis of Systems, pp. 401-416. , Springer | ||
| 504 | |a 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 | ||
| 504 | |a Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P., (2011) Conditional Model Checking, , arXiv preprint arXiv:1109.6926 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Cadar, C., Sen, K., Symbolic execution for software testing: Three decades later (2013) Communications of the ACM, 56 (2), pp. 82-90 | ||
| 504 | |a Castaño, R., Braberman, V., Garbervetsky, D., Uchitel, S., (2016) Model Checker Execution Reports, , arXiv preprint arXiv:1607.06857 | ||
| 504 | |a 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 | ||
| 504 | |a Christakis, M., Müller, P., Wüstholz, V., Collaborative verification and testing with explicit assumptions (2012) FM 2012: Formal Methods, pp. 132-146. , Springer | ||
| 504 | |a Czech, M., Jakobs, M.-C., Wehrheim, H., Just test what you cannot verify (2015) Fundamental Approaches to Software Engineering, pp. 100-114. , Springer | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G., Lazy abstraction (2002) ACM SIGPLAN Notices, 37 (1), pp. 58-70 | ||
| 504 | |a Jackson, D., (2012) Software Abstractions: Logic, Language, and Analysis, , MIT press | ||
| 504 | |a Jhala, R., Majumdar, R., Software model checking (2009) ACM Computing Surveys (CSUR), 41 (4), p. 21 | ||
| 504 | |a 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 | ||
| 504 | |a Lal, A., Qadeer, S., Lahiri, S.K., A solver for reachability modulo theories (2012) International Conference on Computer Aided Verification, pp. 427-443. , Springer | ||
| 504 | |a Leino, K.R.M., Dafny: An automatic program verifier for functional correctness (2010) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348-370. , Springer | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 506 | |2 openaire |e Política editorial | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Departamento de Computación, FCEyN, UBA, CONICET, Buenos Aires, Argentina | ||
| 690 | 1 | 0 | |a SOFTWARE ENGINEERING |
| 690 | 1 | 0 | |a ABSTRACT REACHABILITY TREES |
| 690 | 1 | 0 | |a MODEL CHECKER |
| 690 | 1 | 0 | |a SOFTWARE MODEL CHECKERS |
| 690 | 1 | 0 | |a SOFTWARE MODEL CHECKING |
| 690 | 1 | 0 | |a MODEL CHECKING |
| 700 | 1 | |a Braberman, V. | |
| 700 | 1 | |a Garbervetsky, D. | |
| 700 | 1 | |a Uchitel, Sebastián | |
| 700 | 1 | |a Nguyen T.N. | |
| 700 | 1 | |a Rosu G. | |
| 700 | 1 | |a Di Penta M. | |
| 700 | 1 | |a College of Engineering; Denso; et al.; Microsoft; NASA; University of Minnesota, Software Engineering | |
| 711 | 2 | |d 30 October 2017 through 3 November 2017 |g Código de la conferencia: 132671 | |
| 773 | 0 | |d Institute of Electrical and Electronics Engineers Inc., 2017 |h pp. 200-205 |p ASE - Proc. IEEE/ACM Int. Conf. Autom. Softw. Eng. |n ASE 2017 - Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering |z 9781538626849 |t 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-85041444655&doi=10.1109%2fASE.2017.8115633&partnerID=40&md5=d49fb50654e05292173e1f3bb4881706 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1109/ASE.2017.8115633 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_97815386_v_n_p200_Castano |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97815386_v_n_p200_Castano |y Registro en la Biblioteca Digital |
| 961 | |a paper_97815386_v_n_p200_Castano |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/conferenceObject |a info:ar-repo/semantics/documento de conferencia |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 78410 | ||