Realization and Extension of Abstract Operation Contracts for Program Logic
This work addresses verification efficiency for software engineers, but it is incremental as it builds on a recently proposed rule.
The paper tackles the problem of disproportionate verification effort when software specifications change by implementing and evaluating abstract method calls in the KeY system to enable efficient proof reuse.
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.