Grätz, Lukas ; Hähnle, Reiner ; Bubel, Richard
Hrsg.: Johnsen, Einar Broch ; Wimmer, Manuel (2022)
Finding Semantic Bugs Fast.
25th International Conference of the European Joint Conferences on Theory and Practice of Software. Munich, Germany (02.04.2022-07.04.2022)
doi: 10.1007/978-3-030-99429-7_8
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
Finding semantic bugs in code is difficult and requires precious expert time. Lacking comprehensive formal specifications, deductive verification is not an option. We propose an incremental specification procedure: With the help of automatic verification tools, a domain expert is guided through program runs and source code locations. The expert validates a run at certain locations and creates lightweight annotations. Formal methods training is not required. We demonstrate by example that this approach is capable to quickly detect different kinds of semantic bugs. We position our approach in the middle ground between fully-fledged deductive verification and bug finding without semantic guidance.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2022 |
| Herausgeber: | Johnsen, Einar Broch ; Wimmer, Manuel |
| Autor(en): | Grätz, Lukas ; Hähnle, Reiner ; Bubel, Richard |
| Art des Eintrags: | Bibliographie |
| Titel: | Finding Semantic Bugs Fast |
| Sprache: | Englisch |
| Publikationsjahr: | 29 März 2022 |
| Verlag: | Springer |
| Buchtitel: | Fundamental Approaches to Software Engineering |
| Reihe: | Lecture Notes in Computer Science |
| Band einer Reihe: | 13241 |
| Veranstaltungstitel: | 25th International Conference of the European Joint Conferences on Theory and Practice of Software |
| Veranstaltungsort: | Munich, Germany |
| Veranstaltungsdatum: | 02.04.2022-07.04.2022 |
| DOI: | 10.1007/978-3-030-99429-7_8 |
| URL / URN: | https://doi.org/10.1007/978-3-030-99429-7\_8 |
| Kurzbeschreibung (Abstract): | Finding semantic bugs in code is difficult and requires precious expert time. Lacking comprehensive formal specifications, deductive verification is not an option. We propose an incremental specification procedure: With the help of automatic verification tools, a domain expert is guided through program runs and source code locations. The expert validates a run at certain locations and creates lightweight annotations. Formal methods training is not required. We demonstrate by example that this approach is capable to quickly detect different kinds of semantic bugs. We position our approach in the middle ground between fully-fledged deductive verification and bug finding without semantic guidance. |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 20 Jul 2022 07:21 |
| Letzte Änderung: | 05 Dez 2022 13:00 |
| PPN: | 502287152 |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum