Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
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_ | 1866916380490596352 |
|---|---|
| author | Baier, Daniel Beyer, Dirk Chien, Po-Chun Jakobs, Marie-Christine Jankola, Marek Kettl, Matthias Lee, Nian-Ze Lemberger, Thomas Lingsch-Rosenfeld, Marian Wachowitz, Henrik Wendler, Philipp |
| author_facet | Baier, Daniel Beyer, Dirk Chien, Po-Chun Jakobs, Marie-Christine Jankola, Marek Kettl, Matthias Lee, Nian-Ze Lemberger, Thomas Lingsch-Rosenfeld, Marian Wachowitz, Henrik Wendler, Philipp |
| contents | This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k -induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_02094 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version) Baier, Daniel Beyer, Dirk Chien, Po-Chun Jakobs, Marie-Christine Jankola, Marek Kettl, Matthias Lee, Nian-Ze Lemberger, Thomas Lingsch-Rosenfeld, Marian Wachowitz, Henrik Wendler, Philipp Software Engineering Programming Languages D.2.4; F.3.1; D.3.1; F.4.3 This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k -induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php. |
| title | Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version) |
| topic | Software Engineering Programming Languages D.2.4; F.3.1; D.3.1; F.4.3 |
| url | https://arxiv.org/abs/2409.02094 |