ReVeriX: Efficiently Reverifying Modified Programs Despite of Switching the Verification Approach

• Applicant: Professorin Dr. Marie-Christine Jakobs
• Subject Area: Software Engineering and Programming Languages
• Term: since 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 496852682

Software verification aims at protecting software against violations of properties or specifications by proving the absence of such violations. Since each software change may introduce new violations, modified software needs to be reverified. However, a naive verification of the modified software cannot keep up with the large amount of software changes in long-lived and continuously evolving software projects. To overcome this problem, numerous techniques exist that allow efficient reverification with a particular verification approach. Though, limiting reverification to a particular approach is not desirable. First, verification technology likely advances during the life cycle of long-lived software projects, which makes it necessary to change the verification approach. Second, nowadays many verification tools use more than one verification approach. Thus, the goal of this project is to increase the options for efficient reverification when the verification approach changes.To achieve an efficient reverification despite the change of the verification approach, (1) one must be able to provide information to a different verification approach such that this approach can efficiently reverify the changed software or (2) one needs reverification approaches that are independent of the verification approach. The objective of this project is to examine to which extent one can achieve an efficient reverification despite the change of the verification approach (1) when exchanging information between verification approaches and (2) when restricting any verification approach to relevant, modified paths.The focus of the project are the assurance of safety properties.

• DFG Programme: Research Grants