Reuse in Software Verification by Abstract Method Calls

摘要

A major obstacle facing adoption of formal software verification is the difficulty to track changes in the target code and to accomo-date them in specifications and in verification arguments. We introduce abstract method calls, a new verification rule for method calls that can be used in most contract-based verification settings. By combining abstract method calls, structured reuse in specification contracts, and caching of verification conditions, it is possible to detect reusability of contracts automatically via first-order reasoning. This is the basis for a verification framework that is able to deal with code undergoing frequent changes.