| Autor: |
Lukas Grätz, Reiner Hähnle, Richard Bubel |
| Rok vydání: |
2022 |
| Zdroj: |
Fundamental Approaches to Software Engineering ISBN: 9783030994280 |
| Popis: |
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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
