BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support

Mostrar todas las versiones(2)

In this article we present BLISS, a novel technique that 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 dee...

Descripción completa

Detalles Bibliográficos
Autores principales: Rosner, Nicolás, Geldenhuys, Jaco, Aguirre, Nazareno Matías, Visser, Willem
Formato: Objeto de conferencia Resumen
Lenguaje:Inglés
Publicado: 2016
Materias:
Ciencias Informáticas
Bounded Lazy Initialization (BLI)
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/57306
http://45jaiio.sadio.org.ar/sites/default/files/asse-26.pdf
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-57306
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Bounded Lazy Initialization (BLI)
spellingShingle Ciencias Informáticas
Bounded Lazy Initialization (BLI)
Rosner, Nicolás
Geldenhuys, Jaco
Aguirre, Nazareno Matías
Visser, Willem
BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support
topic_facet Ciencias Informáticas
Bounded Lazy Initialization (BLI)
description In this article we present BLISS, a novel technique that 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 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 4 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%, with reductions of over 90% in some cases (compared to LI). BLISS uses less memory than LI and BLI, which enables the exploration of states unreachable by previous techniques.
format Objeto de conferencia
Resumen
author Rosner, Nicolás
Geldenhuys, Jaco
Aguirre, Nazareno Matías
Visser, Willem
author_facet Rosner, Nicolás
Geldenhuys, Jaco
Aguirre, Nazareno Matías
Visser, Willem
author_sort Rosner, Nicolás
title BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support
title_short BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support
title_full BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support
title_fullStr BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support
title_full_unstemmed BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support
title_sort bliss: improved symbolic execution by bounded lazy initialization with sat support
publishDate 2016
url http://sedici.unlp.edu.ar/handle/10915/57306
http://45jaiio.sadio.org.ar/sites/default/files/asse-26.pdf
work_keys_str_mv AT rosnernicolas blissimprovedsymbolicexecutionbyboundedlazyinitializationwithsatsupport
AT geldenhuysjaco blissimprovedsymbolicexecutionbyboundedlazyinitializationwithsatsupport
AT aguirrenazarenomatias blissimprovedsymbolicexecutionbyboundedlazyinitializationwithsatsupport
AT visserwillem blissimprovedsymbolicexecutionbyboundedlazyinitializationwithsatsupport
bdutipo_str Repositorios
_version_ 1764820478104436736

Ejemplares similares