Component-based CEGAR - Building Software Verifiers from Off-the-Shelf Components
| dc.contributor.author | Beyer, Dirk | |
| dc.contributor.author | Haltermann, Jan | |
| dc.contributor.author | Lemberger, Thomas | |
| dc.contributor.author | Wehrheim, Heike | |
| dc.contributor.editor | Engels, Gregor | |
| dc.contributor.editor | Hebig, Regina | |
| dc.contributor.editor | Tichy, Matthias | |
| dc.date.accessioned | 2023-01-18T13:38:57Z | |
| dc.date.available | 2023-01-18T13:38:57Z | |
| dc.date.issued | 2023 | |
| dc.description.abstract | Software verification tools typically consist of tighly coupled components, thereby precluding the easy integration of off-the-shelf components. We propose to decompose software verification into independent subtasks, each task being implemented by an own component communicating with other components via clearly defined interfaces. We apply this idea of decomposition to one of the most frequently used techniques in software verification: CEGAR. Our decomposition, called component-based CEGAR (C-CEGAR), comprises three components: An abstract model explorer, a feasibility checker and a precision refiner. It allows employing conceptually different components for each task within one instance. Our evaluation shows that C-CEGAR has, compared to a monolithic CEGAR-implementation, a similar efficiency and that the precision in solving verification tasks even increases. | en |
| dc.identifier.isbn | 978-3-88579-726-5 | |
| dc.identifier.pissn | 1617-5468 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/40128 | |
| dc.language.iso | en | |
| dc.publisher | Gesellschaft für Informatik e.V. | |
| dc.relation.ispartof | Software Engineering 2023 | |
| dc.relation.ispartofseries | Lecture Notes in Informatics (LNI) - Proceedings, Volume P-332 | |
| dc.subject | Software engineering | |
| dc.subject | Software verification | |
| dc.subject | Abstraction refinement | |
| dc.subject | CEGAR | |
| dc.subject | Decomposition | |
| dc.subject | Cooperative verification | |
| dc.title | Component-based CEGAR - Building Software Verifiers from Off-the-Shelf Components | en |
| dc.type | Text/Conference Paper | |
| gi.citation.endPage | 38 | |
| gi.citation.publisherPlace | Bonn | |
| gi.citation.startPage | 37 | |
| gi.conference.date | 20.–24. Februar 2023 | |
| gi.conference.location | Paderborn | |
| gi.conference.sessiontitle | Wissenschaftliches Hauptprogramm |
Dateien
Originalbündel
1 - 1 von 1
Vorschaubild nicht verfügbar
- Name:
- paper5.pdf
- Größe:
- 324.15 KB
- Format:
- Adobe Portable Document Format