Grätz, Lukas ; Hähnle, Reiner ; Bubel, Richard
eds.: 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.-07.04.2022)
doi: 10.1007/978-3-030-99429-7_8
Conference or Workshop Item, Bibliographie
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.
| Item Type: | Conference or Workshop Item |
|---|---|
| Erschienen: | 2022 |
| Editors: | Johnsen, Einar Broch ; Wimmer, Manuel |
| Creators: | Grätz, Lukas ; Hähnle, Reiner ; Bubel, Richard |
| Type of entry: | Bibliographie |
| Title: | Finding Semantic Bugs Fast |
| Language: | English |
| Date: | 29 March 2022 |
| Publisher: | Springer |
| Book Title: | Fundamental Approaches to Software Engineering |
| Series: | Lecture Notes in Computer Science |
| Series Volume: | 13241 |
| Event Title: | 25th International Conference of the European Joint Conferences on Theory and Practice of Software |
| Event Location: | Munich, Germany |
| Event Dates: | 02.-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 |
| 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. |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Software Engineering |
| Date Deposited: | 20 Jul 2022 07:21 |
| Last Modified: | 05 Dec 2022 13:00 |
| PPN: | 502287152 |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum