Bubel, Richard ; Hähnle, Reiner ; Pelevina, Maria (2014)
Fully Abstract Operation Contracts.
Conference or Workshop Item, Bibliographie
Abstract
Proof reuse in formal software verification is crucial in presence of constant evolutionary changes to the verification target. Contract-based verification makes it possible to verify large programs, because each method in a program can be verified against its contract separately. A small change to some contract, however, invalidates all proofs that rely on it, which makes reuse difficult. We introduce fully abstract contracts and class invariants which permit to completely decouple reasoning about programs from the applicability check of contracts. We implemented tool support for abstract contracts as part of the KeY verification system and empirically show the considerable reuse potential of our approach.
| Item Type: | Conference or Workshop Item |
|---|---|
| Erschienen: | 2014 |
| Creators: | Bubel, Richard ; Hähnle, Reiner ; Pelevina, Maria |
| Type of entry: | Bibliographie |
| Title: | Fully Abstract Operation Contracts |
| Language: | German |
| Date: | 2014 |
| Publisher: | Springer |
| Book Title: | Proceedings 6th International Symposium On Leveraging Applications of Formal Methods |
| Series: | LNCS |
| Abstract: | Proof reuse in formal software verification is crucial in presence of constant evolutionary changes to the verification target. Contract-based verification makes it possible to verify large programs, because each method in a program can be verified against its contract separately. A small change to some contract, however, invalidates all proofs that rely on it, which makes reuse difficult. We introduce fully abstract contracts and class invariants which permit to completely decouple reasoning about programs from the applicability check of contracts. We implemented tool support for abstract contracts as part of the KeY verification system and empirically show the considerable reuse potential of our approach. |
| Identification Number: | TUD-CS-2014-0834 |
| Divisions: | 20 Department of Computer Science > Software Engineering 20 Department of Computer Science |
| Date Deposited: | 31 Dec 2016 10:40 |
| Last Modified: | 16 May 2018 12:06 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum