Regression verification - A practical way to verify programs

Abstract

Compared with existing C verification tools, all of which are property based, Regression Verification has two things to offer. First, code that cannot be easily checked against a formal specification can still be checked throughout the development process by examining its evolving effect on the output (or, in fact, on internal variables as well, which helps pin-pointing the cause for the difference). Second, comparing two similar systems is in most cases computationally easier than property-based verification2. The reason for this is that there are various optimizations and decomposition opportunities that are only relevant when comparing two closely related systems. We described one such optimization based on Uninterpreted Functions in section 2.3. © IFIP International Federation for Information Processing 2008.