Deductive Verification of Legacy Code
Bernhard Beckert, Thorsten Bormer, and Daniel Grahl
Deductive verification is about proving that a piece of code conforms to a
given requirement specification. For legacy code, this task is notoriously
hard for three reasons: (1) writing specifications posthoc is much more
difficult than producing code and its specification simultaneously, (2)
verification does not scale as legacy code is often badly modularized, (3)
legacy code may be written in a way such that verification requires frequent
user interaction. We give examples for which characteristics of (imperative)
legacy code impede the specification and verification effort. We also discuss
how to handle the challenges of legacy code verification and suggest a
strategy for post-hoc verification, together with possible improvements to
existing verification approaches. We draw our experience from two case studies
for verification of imperative implementations (in Java and C) in which we
verified legacy software, i.e., code that was provided by a third party and
was not designed to be verified.