Path-optimal symbolic execution of heap-manipulating programs
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911375388835840 |
|---|---|
| author | Braione, Pietro Denaro, Giovanni Guglielmo, Luca |
| author_facet | Braione, Pietro Denaro, Giovanni Guglielmo, Luca |
| contents | Symbolic execution is at the core of many techniques for program analysis and test generation. Traditional symbolic execution of programs with numeric inputs enjoys the property of forking as many analysis traces as the number of analyzed program paths, a property that in this paper we refer to as path optimality. On the contrary, current approaches for symbolic execution of heap-manipulating programs fail to satisfy this property, thereby incurring crucial path explosion effects. This paper introduces POSE, path-optimal symbolic execution, a symbolic execution algorithm that originally achieves path optimality against heap-manipulating programs. We formalize the POSE algorithm and experiment it against a benchmark of programs that take data structures as inputs, supporting the potential of POSE for improving on the state of the art of symbolic execution of heap-manipulating programs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_16827 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Path-optimal symbolic execution of heap-manipulating programs Braione, Pietro Denaro, Giovanni Guglielmo, Luca Software Engineering Logic in Computer Science D.2.4; D.2.5 Symbolic execution is at the core of many techniques for program analysis and test generation. Traditional symbolic execution of programs with numeric inputs enjoys the property of forking as many analysis traces as the number of analyzed program paths, a property that in this paper we refer to as path optimality. On the contrary, current approaches for symbolic execution of heap-manipulating programs fail to satisfy this property, thereby incurring crucial path explosion effects. This paper introduces POSE, path-optimal symbolic execution, a symbolic execution algorithm that originally achieves path optimality against heap-manipulating programs. We formalize the POSE algorithm and experiment it against a benchmark of programs that take data structures as inputs, supporting the potential of POSE for improving on the state of the art of symbolic execution of heap-manipulating programs. |
| title | Path-optimal symbolic execution of heap-manipulating programs |
| topic | Software Engineering Logic in Computer Science D.2.4; D.2.5 |
| url | https://arxiv.org/abs/2407.16827 |