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: | Acta de conferencia 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 | 09631caa a22010817a 4500 | ||
|---|---|---|---|
| 001 | PAPER-14697 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518204516.0 | ||
| 008 | 190411s2014 xx ||||fo|||| 10| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-84908297069 | |
| 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 | ||
| 270 | 1 | 0 | |m Rosner, N.; Dept. of Computer Science FCEyN, University of Buenos AiresArgentina |
| 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 (2005) ICSE | ||
| 504 | |a Galeotti, J.P., Rosner, N., López 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 (2012) ICFEM | ||
| 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 ASE 2011, , (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 The HyTeK Distribution Can Be Downloaded, , http://bonnie.exp.dc.uba.ar/hytek-oopsla.tar.gz | ||
| 504 | |a http://alloy.mit.edu/A4 - ACM SIGPLAN | ||
| 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. Copyright 2014 ACM. 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. |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 Dept. of Computer Science FCEFQyN, University of Rio Cuarto and CONICET, Rio-Cuarto, Argentina | ||
| 593 | |a Dept. of Software Engineering, Instituto Tecnólogico de Buenos Aires and 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 COMPUTER PROGRAMMING LANGUAGES |
| 690 | 1 | 0 | |a COMPUTER SYSTEMS PROGRAMMING |
| 690 | 1 | 0 | |a SOFTWARE TESTING |
| 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 OBJECT ORIENTED PROGRAMMING |
| 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. | |
| 711 | 2 | |d 20 October 2014 through 24 October 2014 |g Código de la conferencia: 108613 | |
| 773 | 0 | |d Association for Computing Machinery, 2014 |h pp. 655-674 |p Proc Conf Object Orient Program Syst Lang Appl OOPSLA |n Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA |z 9781450325851 |t 2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84908297069&doi=10.1145%2f2660193.2660232&partnerID=40&md5=8b4ae4c2b567613f5861658f875aeb9f |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_97814503_v_n_p655_Rosner |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97814503_v_n_p655_Rosner |y Registro en la Biblioteca Digital |
| 961 | |a paper_97814503_v_n_p655_Rosner |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 75650 | ||