Our current research topics
Software is modified regularly. Bugs get fixed, new functionality is added or existing functionality is adapted. After each change, the software must be verified. Instead of restarting the verification from scratch, incremental verification aims at using information from previous verification runs to simplify the verification of the modified software.
In part project L of Software-Factory 4.0, we want to apply formal methods to check whether sequential and parallelized program (the modified program) are functional equivalent.
In cooperation with the research group of Prof. Dirk Beyer, we study techniques that aim at the verification of modified paths only. To this end, we develop approaches that identify modified paths and output them in an exchangeable format (named condition). Then, the verifier is guided by the condition to only explore modified paths.
Combination of Verification Approaches
Verifiers have different strength and weaknesses. For some programs, none of the existing, single verifiers is sufficient to verify the program. Instead of developing new, better verifiers, we aim at an easy combination of existing verifiers.
Together with the groups of Prof. Dirk Beyer and Prof. Heike Wehrheim, we develop techniques for cooperative software verification. We are interested in the following research questions: To cooperate successfully, which information should be exchanged between verifiers and how? What must be done to let an arbitrary verifier make use of exchanged information? How to combine information resulting from different cooperation partners? To answer some of these questions we consider the idea of conditional model checking.
With our CoVeriTest, we additionally study the combination of verifiers for the purpose of test-case generation.
Validation of Verification Results
A verification result are not always correct. Bugs in the verifier, wrong assumptions, or conceptual weaknesses of the verification approach may result in wrong answers, either a false alarm (non-existing error) or a false proof. Instead of trusting the verifier‘s result, one should require that the verifier provides evidence for its results and check this evidence independently.
In the past, we mainly focused on providing evidence for and checking results from the verification of sequential programs. Our current focus is on explaining and checking results of the verification of parallel programs.