Summary
Software updates are a fact of life, yet they are difficult for developers to get right because the new version must correctly interact with the previous version. Incorrect updates remain a surprisingly common source of catastrophic failures in practice. Formal verification, a technique where software is mathematically proven to behave as intended, is a promising approach to make software more reliable; however, with existing verification approaches, we don't know how to state (much less prove) compatibility. This project's novelties are to develop a definition of software update correctness a
