Bubel, Richard ; Hähnle, Reiner ; Pelevina, Maria (2014)
Fully Abstract Operation Contracts.
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2014 |
| Autor(en): | Bubel, Richard ; Hähnle, Reiner ; Pelevina, Maria |
| Art des Eintrags: | Bibliographie |
| Titel: | Fully Abstract Operation Contracts |
| Sprache: | Deutsch |
| Publikationsjahr: | 2014 |
| Verlag: | Springer |
| Buchtitel: | Proceedings 6th International Symposium On Leveraging Applications of Formal Methods |
| Reihe: | LNCS |
| Kurzbeschreibung (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. |
| ID-Nummer: | TUD-CS-2014-0834 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik > Software Engineering 20 Fachbereich Informatik |
| Hinterlegungsdatum: | 31 Dez 2016 10:40 |
| Letzte Änderung: | 16 Mai 2018 12:06 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum