Current Projects
ReVeriX: Efficiently Reverifying Modified Programs Despite of Switching the Verification Approach (DFG Project)
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 longlived 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.
Past Projects
Software systems play an important role in today’s economy and society and existing software systems are challenged by new requirements and environmental changes. To deal with these challenges, the LOEWE project Software-Factory 4.0 aims at developing innovative concepts, techniques, and tools to support mostly automatic reengineering of software. The three main research goals are: flexibilization of specialized software systems, parallelization of software, and simplification of the reengineering.
The research group semantics and verification of parallel systems contributes to part project L in Software-Factory 4.0. Part project L looks into the functional correctness of the parallelized program. It focus is on the functional equivalence between sequential and parallelized program.
The LOEWE project Software-Factory 4.0 is a 4-year project funded by the German State of Hesse.