Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2302.02382 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866908405194555392 |
|---|---|
| author | Emrich, Frank Hensel, Jera Giesl, Jürgen |
| author_facet | Emrich, Frank Hensel, Jera Giesl, Jürgen |
| contents | Termination analysis of C programs is a challenging task. On the one hand, the analysis needs to be precise enough to draw meaningful conclusions. On the other hand, relevant programs in practice are large and require substantial abstraction. It is this inherent trade-off that is the crux of the problem. In this work, we present AProVE, a tool that uses symbolic execution to analyze termination of memory-manipulating C programs. While traditionally, AProVE's focus was on the preciseness of the analysis, we describe how we adapted our approach towards a modular analysis. Due to this adaption, our approach can now also handle recursive programs. Moreover, we present further performance improvements which we developed to make AProVE scale to large programs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2302_02382 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | AProVE: Modular Termination Analysis of Memory-Manipulating C Programs Emrich, Frank Hensel, Jera Giesl, Jürgen Logic in Computer Science Termination analysis of C programs is a challenging task. On the one hand, the analysis needs to be precise enough to draw meaningful conclusions. On the other hand, relevant programs in practice are large and require substantial abstraction. It is this inherent trade-off that is the crux of the problem. In this work, we present AProVE, a tool that uses symbolic execution to analyze termination of memory-manipulating C programs. While traditionally, AProVE's focus was on the preciseness of the analysis, we describe how we adapted our approach towards a modular analysis. Due to this adaption, our approach can now also handle recursive programs. Moreover, we present further performance improvements which we developed to make AProVE scale to large programs. |
| title | AProVE: Modular Termination Analysis of Memory-Manipulating C Programs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2302.02382 |