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

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 in...

Descripción completa

Detalles Bibliográficos
Autores principales: Rosner, N., Geldenhuys, J., Aguirre, N.M., Visser, W., Frias, M.F.
Formato: JOUR
Materias:
lazy initialization
Symbolic execution
Symbolic PathFinder
tight field bounds
Concretes
Data structures
Formal logic
Complex data structures
Novel techniques
Orders of magnitude
Satisfiability
Model checking
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_00985589_v41_n7_p639_Rosner
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_00985589_v41_n7_p639_Rosner
record_format dspace
spelling todo:paper_00985589_v41_n7_p639_Rosner2023-10-03T14:56:59Z BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support Rosner, N. Geldenhuys, J. Aguirre, N.M. Visser, W. Frias, M.F. 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 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. Fil:Rosner, N. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Frias, M.F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_00985589_v41_n7_p639_Rosner
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic 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
spellingShingle 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
Rosner, N.
Geldenhuys, J.
Aguirre, N.M.
Visser, W.
Frias, M.F.
BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support
topic_facet 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
description 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.
format JOUR
author Rosner, N.
Geldenhuys, J.
Aguirre, N.M.
Visser, W.
Frias, M.F.
author_facet Rosner, N.
Geldenhuys, J.
Aguirre, N.M.
Visser, W.
Frias, M.F.
author_sort Rosner, N.
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
url http://hdl.handle.net/20.500.12110/paper_00985589_v41_n7_p639_Rosner
work_keys_str_mv AT rosnern blissimprovedsymbolicexecutionbyboundedlazyinitializationwithsatsupport
AT geldenhuysj blissimprovedsymbolicexecutionbyboundedlazyinitializationwithsatsupport
AT aguirrenm blissimprovedsymbolicexecutionbyboundedlazyinitializationwithsatsupport
AT visserw blissimprovedsymbolicexecutionbyboundedlazyinitializationwithsatsupport
AT friasmf blissimprovedsymbolicexecutionbyboundedlazyinitializationwithsatsupport
_version_ 1807323168253149184

Ejemplares similares