Formal verifcation of evolving software
Verified software usually consists of
- a formal specification
- an implementation (in the same or a different language than the specification)
- a proof that the latter conforms to the former
When the specification changes, the typical practice is to publish new revisions of all three and move the old versions to history.
However, if the old version of the software has been heavily used, it may not be possible to simply replace it. For example, if the old version was used to process input, it is not guaranteed at all that the new version will interpret the legacy input in exactly the same way as the old one did (even if the new implementation conforms to the new specification). Instead, it is necessary to additionally relate the semantics of old and new version.
Very little theoretical work and/or practical tools for this change management problem exist.
In this project, you will solve this problem for a simple language (as complicated as we can manage) and develop a method for establishing formal theorems that relate old and new version.