Navegar

Colección

Datos Estadísticas

Artículo

Rosner, N.; Geldenhuys, J.; Aguirre, N.M.; Visser, W.; Frias, M.F. "BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support" (2015) IEEE Transactions on Software Engineering. 41(7):639-660
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Lazy Initialization (LI) allows symbolic execution to effectively deal with heap-allocated data structures, thanks to a significant reduction in spurious and redundant symbolic structures. Bounded lazy initialization (BLI) improves on LI by taking advantage of precomputed relational bounds on the interpretation of class fields in order to reduce the number of spurious structures even further. In this paper we present bounded lazy initialization with SAT support (BLISS), a novel technique that refines the search for valid structures during the symbolic execution process. BLISS builds upon BLI, extending it with field bound refinement and satisfiability checks. Field bounds are refined while a symbolic structure is concretized, avoiding cases that, due to the concrete part of the heap and the field bounds, can be deemed redundant. Satisfiability checks on refined symbolic heaps allow us to prune these heaps as soon as they are identified as infeasible, i.e., as soon as it can be confirmed that they cannot be extended to any valid concrete heap. Compared to LI and BLI, BLISS reduces the time required by LI by up to four orders of magnitude for the most complex data structures. Moreover, the number of partially symbolic structures obtained by exploring program paths is reduced by BLISS by over 50 percent, with reductions of over 90 percent in some cases (compared to LI). BLISS uses less memory than LI and BLI, which enables the exploration of states unreachable by previous techniques. © 1976-2012 IEEE.

Registro:

Documento: Artículo
Título:BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support
Autor:Rosner, N.; Geldenhuys, J.; Aguirre, N.M.; Visser, W.; Frias, M.F.
Filiación:Department of Computer Science, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina
Department of Computer Science, University of Stellenbosch, Stellenbosch, South Africa
Department of Computer Science, FCEFQyN, Universidad Nacional de Rio Cuarto, CONICET, Río Cuarto, Argentina
Department of Software Engineering, Instituto Tecnológico de Buenos Aires, CONICET, Buenos Aires, Argentina
Palabras clave:lazy initialization; Symbolic execution; Symbolic PathFinder; tight field bounds; Concretes; Data structures; Formal logic; Complex data structures; lazy initialization; Novel techniques; Orders of magnitude; Satisfiability; Symbolic execution; Symbolic PathFinder; tight field bounds; Model checking
Año:2015
Volumen:41
Número:7
Página de inicio:639
Página de fin:660
DOI: http://dx.doi.org/10.1109/TSE.2015.2389225
Título revista:IEEE Transactions on Software Engineering
Título revista abreviado:IEEE Trans Software Eng
ISSN:00985589
CODEN:IESED
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v41_n7_p639_Rosner

Referencias:

  • Boyapati, C., Khurshid, S., Marinov, D., Korat: Automated testing based on java predicates (2002) Proc. ACM SIGSOFT Int. Symp. Softw. Testing Anal, pp. 123-133
  • Cadar, C., Dunbar, D., Engler, D., Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs (2008) Proc. 8th USENIX Conf. Oper. Syst. Des. Implementation, pp. 209-224
  • Cadar, C., Godefroid, P., Khurshid, S., Pasareanu, C., Sen, K., Tillmanni, N., Visserr, W., Symbolic execution for software testing in practice: Preliminary assessment (2011) Proc. 33rd Int. Conf. Softw. Eng, pp. 1066-1071
  • Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E., Beyond assertions: Advanced specification and verification with jml and esc/java2 (2005) Proc. 4th Int. Conf. Formal Methods Components Objects, pp. 342-363
  • Clarke, E.M., Grumberg, O., Peled, D., (1999) Model Checking, , Cambridge MA USA MIT Press
  • Deng, X., Lee And Robby, J., Bogor/kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems (2006) Proc. 21st IEEE/ACM Int. Conf. Autom. Softw. Eng, pp. 157-166
  • Deng Robby, X., Hatcliff, J., Towards a case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs (2007) Proc. 5th Int. Conf. Softw. Eng. Formal Methods, pp. 273-282
  • Dennis, G., Yessenov, K., Jackson, D., Bounded verification of voting software (2008) Proc. 2nd Int. Conf. Verified Softw.: Theories, Tools, Exp, pp. 130-145
  • Flanagan, C., Leino, R., Lillibridge, M., Nelson, G., Saxe, J., Stata, R., Extended static checking for java (2002) Proc. ACM SIGPLAN Conf. Program. Lang. Des. Implementation
  • Galeotti, J.P., Rosner, N., Lopez Pombo, C., Frias, M.F., Analysis of invariants for efficient bounded verification (2010) Proc. 19th Int. Symp. Softw. Testing Anal, pp. 234-245
  • Galeotti, J.P., Rosner, N., Lopez Pombo, C., Frias, M.F., Taco: Efficient sat-based bounded verification using symmetry breaking and tight bounds (2013) IEEE Trans. Softw. Eng, 39 (9), pp. 1283-1307. , Sep
  • Geldenhuys, J., Aguirre, N., Frias, M.F., Visser, W., Bounded lazy initialization (2013) Proc. 5th Int. NASA Formal Methods Symp, pp. 229-243
  • Jackson, D., Vaziri, M., Finding bugs with a constraint solver (2000) Proc. ACM SIGSOFT Int. Symp. Softw. Testing Anal, pp. 14-25
  • Khurshid, S., Pasareanu, C., Visser, W., Generalized symbolic execution for model checking and testing (2003) Proc. 9th Int. Conf. Tools Algorithms Construction Anal. Syst, pp. 553-568
  • King, J.C., Symbolic execution and program testing (1976) Commun. ACM, 19 (7), pp. 385-394
  • Staats, M., Pasareanu, C.S., Parallel symbolic execution for structural test generation (2010) Proc. 19th Int. Symp. Softw. Testing Anal, pp. 183-194
  • Psreanu, C.S., Visser, W., Bushnell, D., Geldenhuys, J., Mehlitz, P., Rungta, N., Symbolic pathfinder: Integrating symbolic execution with model checking for java bytecode analysis (2013) Autom. Softw. Eng, 20 (3), pp. 391-425
  • (2015) Redis Can Be Downloaded from, , http://redis.io/download, [Online]. Available
  • Rosner, N., Galeotti, J.P., Bermudez, S., Blas, G.M., Rosso De S.Perez, Pizzagalli L Zemn, L., Frias, M.F., Parallel bounded analysis in code with rich invariants by refinement of field bounds (2013) Proc. Int. Symp. Softw. Testing Anal, pp. 23-33
  • Shao, D., Khurshid, S., Perry, D., Whispec: White-box testing of libraries using declarative specifications (2007) Proc. Symp. Library-Centric Softw. des, pp. 11-20
  • Vaziri, M., Jackson, D., Checking properties of heap-manipulating procedures with a constraint solver (2003) Proc. 9th Int. Conf. Tools Algorithms Construction Anal. Syst, pp. 505-520
  • Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F., Model checking programs (2003) Autom. Softw. Eng, 10 (2), pp. 203-232
  • Visser, W., Pasareanu, C., Khurshid, S., Test input generation with java pathfinder (2004) Proc. ACM SIGSOFT Int. Symp. Softw. Testing Anal, pp. 97-107
  • Visser, W., Geldenhuys, J., Dwyer, M.B., Green: Reducing, reusing and recycling constraints in program analysis Proc. ACM SIGSOFT Symp. Foundations Softw. Eng, 2012, pp. 58-69
  • (2015), http://www.satcompetition.org/2009/format-benchmarks2009.html, [Online]. Available; (2015), http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc, [Online]. Available

Citas:

---------- APA ----------
Rosner, N., Geldenhuys, J., Aguirre, N.M., Visser, W. & Frias, M.F. (2015) . BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support. IEEE Transactions on Software Engineering, 41(7), 639-660.
http://dx.doi.org/10.1109/TSE.2015.2389225
---------- CHICAGO ----------
Rosner, N., Geldenhuys, J., Aguirre, N.M., Visser, W., Frias, M.F. "BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support" . IEEE Transactions on Software Engineering 41, no. 7 (2015) : 639-660.
http://dx.doi.org/10.1109/TSE.2015.2389225
---------- MLA ----------
Rosner, N., Geldenhuys, J., Aguirre, N.M., Visser, W., Frias, M.F. "BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support" . IEEE Transactions on Software Engineering, vol. 41, no. 7, 2015, pp. 639-660.
http://dx.doi.org/10.1109/TSE.2015.2389225
---------- VANCOUVER ----------
Rosner, N., Geldenhuys, J., Aguirre, N.M., Visser, W., Frias, M.F. BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support. IEEE Trans Software Eng. 2015;41(7):639-660.
http://dx.doi.org/10.1109/TSE.2015.2389225