TU Darmstadt / ULB / TUbiblio

Fully Abstract Operation Contracts

Bubel, Richard and Hähnle, Reiner and Pelevina, Maria (2014):
Fully Abstract Operation Contracts.
In: LNCS, In: Proceedings 6th International Symposium On Leveraging Applications of Formal Methods, Springer, [Conference or Workshop Item]

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 and Hähnle, Reiner and Pelevina, Maria
Title: Fully Abstract Operation Contracts
Language: German
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.

Title of Book: Proceedings 6th International Symposium On Leveraging Applications of Formal Methods
Series Name: LNCS
Publisher: Springer
Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Date Deposited: 31 Dec 2016 10:40
Identification Number: TUD-CS-2014-0834
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)

View Item View Item