The goal of this project is to leverage advances in deductive program verification to enable regression verification, i.e., proving formally that software remains correct through its evolution, and no new bugs are introduced.

We aim to develop a regression verification methodology for a real object-oriented language (Java) that has the reach and power to be applied to real-world software. Even though building software with high quality from the beginning of the software lifecycle is crucial, it is not enough, since long-living software is adapted and evolves during its development and after its release. While traditional regression testing techniques are commonly used to give confidence in the reliability of evolving software, more powerful and reliable techniques are required.

Over the last decade, there has been tremendous progress in the area of program verification. However, in the development of formal methods not enough attention has been given to software changes, which occur during software evolution. A very promising solution is to develop regression verification methods. They are a natural extension of regression testing. Given two programs that are both complex but similar to each other, much less effort is required to prove their equivalence than to prove that they satisfy a (complex) functional specification. The effort for proving equivalence mainly depends on the difference between the programs and not on their overall size and complexity.

Our vision and goal is to develop regression verification methods powerful enough to be applicable to real-word software (and its evolution). We will develop regression verification methods for Java that can be used to prove that two Java programs are equivalent. We also address the problem of changing requirements by proving that two programs are not fully equivalent but differ in a formally specified way. We will implement these methods in a regression verification system based on our Java verification tool KeY.

Regression verification shows its power (and only makes sense) as part of software evolution. It is central to the success of the proposed project that we integrate our methods into the software development and adaptation process. In particular, we plan to integrate regression verification with refactoring and reengineering of software, with software product line techniques, and with test generation and test selection.

Our project thus addresses the priority programme's guiding theme of methods and processes, contributing to the programme topics of (a) model-based and model-driven development of long-living systems, (b) traceability from requirements to architecture and code, and (c) continuous software system evolution under design (and to a lesser extent also runtime) control and management. We link to the application domains using case studies from the area of information systems, in particular the priority-programme-wide CoCoME case study.