Realization and Extension of Abstract Operation Contracts for Program Logic

TL;DR

This paper enhances the KeY verification system by implementing and extending abstract operation contracts, enabling more efficient reuse of correctness proofs in software verification despite code or specification changes.

Contribution

It introduces new extensions to abstract operation contracts within KeY, improving proof reuse efficiency in formal software correctness verification.

Findings

Extended the KeY system with new abstract operation contract features

Demonstrated improved proof reuse efficiency in case studies

Validated the approach's effectiveness in software verification scenarios

Abstract

For engineering software with formal correctness proofs it is crucial that proofs can be efficiently reused in case the software or its specification is changed. Unfortunately, in reality even slight changes in the code or its specification often result in disproportionate waste of verification effort: For instance, whenever a method's specification is modified and as a consequence the proof of its correctness breaks, all other proofs based on this specification break too. Abstract method calls is a recently proposed verification rule for method calls that allows for efficient systematic reuse of proofs. In this thesis, we implement, extend and evaluate this approach within the KeY verification system.