Bounded exhaustive test input generation from hybrid invariants
We present a novel technique for producing bounded exhaustive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperati...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , , , , , |
| Formato: | Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
Association for Computing Machinery
2014
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 08981caa a22010097a 4500 | ||
|---|---|---|---|
| 001 | PAPER-14696 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518204516.0 | ||
| 008 | 190411s2014 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-84920764998 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Rosner, N. | |
| 245 | 1 | 0 | |a Bounded exhaustive test input generation from hybrid invariants |
| 260 | |b Association for Computing Machinery |c 2014 | ||
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Abad, P., Aguirre, N., Bengolea, V.S., Ciolek, D., Frias, M.F., Galeotti, J.P., Maibaum, T., Vissani, I., Improving test generation under rich contracts by tight bounds and incremental SAT solving (2013) ICST | ||
| 504 | |a Boyapati, C., Khurshid, S., Marinov, D., Korat: Automated testing based on java predicates (2002) ISSTA | ||
| 504 | |a Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Rustan, K., Poll, E., An overview of JML tools and applications (2005) STTT, 7 (3). , Springer | ||
| 504 | |a Chang, F.S.-H., Jackson, D., Symbolic model checking of declarative relational models (2006) ICSE | ||
| 504 | |a Claessen, K., Hughes, J., QuickCheck: A lightweight tool for random testing of haskell programs (2000) ICFP | ||
| 504 | |a De Moura, L., Bjørner, N., Z3: An efficient SMT solver (2008) TACAS | ||
| 504 | |a Dennis, G., Chang, F., Jackson, D., Verification of code with SAT (2006) ISSTA 2006, , ACM | ||
| 504 | |a Dutertre, B., Moura, L.D., (2006) The Yices SMT Solver, , Technical report | ||
| 504 | |a Een, N., Sorensson, N., An extensible SAT-solver (2003) SAT | ||
| 504 | |a Frias, M., Galeotti, J., Pombo, C., Aguirre, N., DynAlloy: Upgrading alloy with actions ICSE 2005 | ||
| 504 | |a Galeotti, J.P., Rosner, N., Lopez Pombo, C., Frias, M., TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds (2013) IEEE TSE, 39 (9), pp. 1283-1307 | ||
| 504 | |a Ganov, S., Khurshid, S., Perry, D.E., Annotations for alloy: Automated incremental analysis using domain specific solvers ICFEM 2012 | ||
| 504 | |a Geldenhuys, J., Aguirre, N., Frias, M.F., Visser, W., Bounded lazy initialization (2013) NFM 2013, , LNCS, Springer | ||
| 504 | |a Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D., Test generation through programming in UDITA (2010) ICSE, , Cape Town, South Africa | ||
| 504 | |a Holzmann, G.J., The model checker SPIN (1997) IEEE TSE | ||
| 504 | |a Jackson, D., (2006) Software Abstractions: Logic, Language and Analysis, , The MIT Press | ||
| 504 | |a Kaner, C., Bach, J., Pettichord, B., (2001) Lessons Learned in Software Testing, , Wiley | ||
| 504 | |a Khalek, S.A., (2011) Systematic Testing Using Test Summaries: Effective and Efficient Testing of Relational Applications, , Ph.D. Thesis. University of Texas at Austin | ||
| 504 | |a Khalek, S.A., Narayanan, V.P., Khurshid, S., Mixed constraints for test input generation - An initial exploration (2011) ASE, , (Short paper) | ||
| 504 | |a Khalek, S.A., Yang, G., Zhang, L., Marinov, D., Khurshid, S., TestEra: A tool for testing java programs using alloy specifications (2011) ASE 2011, , IEEE | ||
| 504 | |a Khurshid, S., Marinov, D., TestEra: Specification-based testing of java programs using SAT (2004) Automated Software Engineering, 11 (4). , Springer | ||
| 504 | |a Koksal, A.S., Kuncak, V., Suter, P., Constraints as control (2012) POPL | ||
| 504 | |a Liskov, B., Guttag, J., (2000) Program Development in Java: Abstraction, Specification, and Object-Oriented Design, , Addison-Wesley | ||
| 504 | |a Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S., Korat: A tool for generating structurally complex test inputs (2007) ICSE 2007, , IEEE Press | ||
| 504 | |a Milicevic, A., Rayside, D., Yessenov, K., Jackson, D., Unifying execution of imperative and declarative code (2011) ICSE | ||
| 504 | |a Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T., Feedback-directed random test generation (2007) ICSE 2007, , IEEE | ||
| 504 | |a Rosner, N., López Pombo, C.G., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F., Parallel bounded verification of alloy models by TranScoping (2013) VSTTE 2014, , LNCS, Springer | ||
| 504 | |a Samimi, H., Aung, E.D., Millstein, T.D., Falling back on executable specifications (2010) ECOOP | ||
| 504 | |a Siddiqui, J., Khurshid, S., An empirical study of structural constraint solving techniques (2009) ICFEM 2009, , LNCS, Springer | ||
| 504 | |a Uzuncaova, E., (2008) Efficient Specification-based Testing Using Incremental Techniques, , PhD thesis, UT@Austin | ||
| 504 | |a Uzuncaova, E., Khurshid, S., Constraint prioritization for efficient analysis of declarative models (2008) FM | ||
| 504 | |a Visser, W., Pəsəreanu, C., Khurshid, S., Test input generation with java PathFinder (2004) ISSTA 2004, , ACM | ||
| 504 | |a Xie, T., Marinov, D., Notkin, D., Rostra: A framework for detecting redundant object-oriented unit tests (2004) ASE 2004, , IEEE | ||
| 504 | |a Zaeem, R.N., Khurshid, S., Contract-based data structure repair using alloy (2010) ECOOP | ||
| 504 | |a http://bonnie.exp.dc.uba.ar/hytek-oopsla.tar.gz, The HyTeK distribution can be downloaded from; http://alloy.mit.edu/ | ||
| 520 | 3 | |a We present a novel technique for producing bounded exhaustive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperative and declarative parts, but combined in a way that enables us to exploit information from the declarative side, such as tight bounds computed from the declarative specification, to improve the search both on the imperative and declarative sides. Moreover, our technique automatically evaluates different possible ways of processing the imperative side, and the alternative settings (imperative or declarative) for parts of the invariant available both declaratively and imperatively, to decide the most convenient invariant configuration with respect to efficiency in test generation. This is achieved by transcoping, i.e., by assessing the efficiency of the different alternatives on small scopes (where generation times are negligible), and then extrapolating the results to larger scopes. We also show experiments involving collection classes that support the effectiveness of our technique, by demonstrating that (i) bounded exhaustive suites can be computed from hybrid invariants significantly more efficiently than doing so using state-of-the-art purely imperative and purely declarative approaches, and (ii) our technique is able to automatically determine efficient hybrid invariants, in the sense that they lead to an efficient computation of bounded exhaustive suites, using transcoping. Copyright © 2014 ACM. |l eng | |
| 536 | |a Detalles de la financiación: National Science Foundation, NSF, CCF-0845628 | ||
| 536 | |a Detalles de la financiación: National Science Foundation, NSF, CNS-1239498 | ||
| 593 | |a Dept. of Computer Science, FCEyN, University of Buenos Aires, Buenos Aires, Argentina | ||
| 593 | |a Dept. of Computer Science, FCEFQyN, University of Rio Cuarto, Rio Cuarto, Argentina | ||
| 593 | |a Google, United States | ||
| 593 | |a CONICET, Rio Cuarto, Argentina | ||
| 593 | |a Dept. of Software Engineering, Instituto Tecnólogico de Buenos Aires, CONICET, Buenos Aires, Argentina | ||
| 593 | |a Electrical and Computer Engineering, University of Texas at Austin, Austin, United States | ||
| 690 | 1 | 0 | |a ALLOY |
| 690 | 1 | 0 | |a AUTOMATED TEST GENERATION |
| 690 | 1 | 0 | |a BOUNDED EXHAUSTIVE TESTING |
| 690 | 1 | 0 | |a KORAT |
| 690 | 1 | 0 | |a SAT SOLVING |
| 690 | 1 | 0 | |a TRANSCOPING |
| 690 | 1 | 0 | |a ALLOYING |
| 690 | 1 | 0 | |a SPECIFICATIONS |
| 690 | 1 | 0 | |a AUTOMATED TEST GENERATIONS |
| 690 | 1 | 0 | |a BOUNDED EXHAUSTIVE TESTING |
| 690 | 1 | 0 | |a KORAT |
| 690 | 1 | 0 | |a SAT-SOLVING |
| 690 | 1 | 0 | |a TRANSCOPING |
| 690 | 1 | 0 | |a SOFTWARE TESTING |
| 700 | 1 | |a Bengolea, V. | |
| 700 | 1 | |a Ponzio, P. | |
| 700 | 1 | |a Khalek, S.A. | |
| 700 | 1 | |a Aguirre, N. | |
| 700 | 1 | |a Frias, M.F. | |
| 700 | 1 | |a Khurshid, S. | |
| 773 | 0 | |d Association for Computing Machinery, 2014 |g v. 49 |h pp. 655-674 |k n. 10 |p ACM SIGPLAN Not. |x 15232867 |t ACM SIGPLAN Notices | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84920764998&doi=10.1145%2f2660193.2660232&partnerID=40&md5=72c4fa138df8de65957cc8796c2ff76d |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1145/2660193.2660232 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_15232867_v49_n10_p655_Rosner |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15232867_v49_n10_p655_Rosner |y Registro en la Biblioteca Digital |
| 961 | |a paper_15232867_v49_n10_p655_Rosner |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 75649 | ||