Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds

Software model checkers are able to exhaustively explore different bounded program executions arising from various sources of nondeterminism. These tools provide statements to produce non-determinis- tic values for certain variables, thus forcing the corresponding model checker to consider all possi...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Ponzio, Pablo Daniel, Godio, Ariel, Rosner, Nicolás, Arroyo, Marcelo, Aguirre, Nazareno Matías, Frias, Marcelo F.
Formato: Objeto de conferencia
Lenguaje:Español
Publicado: 2021
Materias:
Ciencias Informáticas
Model checking of programs
Relational bounds
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/140433
http://50jaiio.sadio.org.ar/pdfs/asse/ASSE-12.pdf
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-140433
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Español
topic Ciencias Informáticas
Model checking of programs
Relational bounds
spellingShingle Ciencias Informáticas
Model checking of programs
Relational bounds
Ponzio, Pablo Daniel
Godio, Ariel
Rosner, Nicolás
Arroyo, Marcelo
Aguirre, Nazareno Matías
Frias, Marcelo F.
Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds
topic_facet Ciencias Informáticas
Model checking of programs
Relational bounds
description Software model checkers are able to exhaustively explore different bounded program executions arising from various sources of nondeterminism. These tools provide statements to produce non-determinis- tic values for certain variables, thus forcing the corresponding model checker to consider all possible values for these during verification. While these statements offer an effective way of verifying programs handling basic data types and simple structured types, they are inappropriate as a mechanism for nondeterministic generation of pointers, favoring the use of insertion routines to produce dynamic data structures when verifying, via model checking, programs handling such data types. We present a technique to improve model checking of programs handling heap-allocated data types, by taming the explosion of candidate structures that can be built when non-deterministically initializing heap object fields. The technique exploits precomputed relational bounds, that disregard values deemed invalid by the structure’s type invariant, thus reducing the state space to be explored by the model checker. Precomputing the relational bounds is a challenging costly task too, for which we also present an efficient algorithm, based on incremental SAT solving. We implement our approach on top of the CBMC bounded model checker, and show that, for a number of data structures implementations, we can handle significantly larger input structures and detect faults that CBMC is unable to detect.
format Objeto de conferencia
Objeto de conferencia
author Ponzio, Pablo Daniel
Godio, Ariel
Rosner, Nicolás
Arroyo, Marcelo
Aguirre, Nazareno Matías
Frias, Marcelo F.
author_facet Ponzio, Pablo Daniel
Godio, Ariel
Rosner, Nicolás
Arroyo, Marcelo
Aguirre, Nazareno Matías
Frias, Marcelo F.
author_sort Ponzio, Pablo Daniel
title Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds
title_short Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds
title_full Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds
title_fullStr Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds
title_full_unstemmed Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds
title_sort efficient bounded model checking of heap-manipulating programs using tight field bounds
publishDate 2021
url http://sedici.unlp.edu.ar/handle/10915/140433
http://50jaiio.sadio.org.ar/pdfs/asse/ASSE-12.pdf
work_keys_str_mv AT ponziopablodaniel efficientboundedmodelcheckingofheapmanipulatingprogramsusingtightfieldbounds
AT godioariel efficientboundedmodelcheckingofheapmanipulatingprogramsusingtightfieldbounds
AT rosnernicolas efficientboundedmodelcheckingofheapmanipulatingprogramsusingtightfieldbounds
AT arroyomarcelo efficientboundedmodelcheckingofheapmanipulatingprogramsusingtightfieldbounds
AT aguirrenazarenomatias efficientboundedmodelcheckingofheapmanipulatingprogramsusingtightfieldbounds
AT friasmarcelof efficientboundedmodelcheckingofheapmanipulatingprogramsusingtightfieldbounds
bdutipo_str Repositorios
_version_ 1764820458827415552

Ejemplares similares