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.
Optimizing Runtime Verification
Runtime Verification is a popular approach to ensure that programs meet certain correctness properties. To this end, a monitor observes the program execution and reacts when a property violation is about to occur. Observing a single execution simplifies the analysis and can make it more precise because information about the execution can be used. In contrast, the monitor introduces a performance overhead. At worst, the overhead is so large that monitoring is no longer practical. Therefore, optimizations for runtime verification aim at reducing the performance overhead.
Together with the research group of Prof. Dr. Heiko Mantel we develop approaches to optimize runtime verification. We also formally prove that the optimizations do not violate runtime verification properties like soundness. Furthermore, we go beyond experimental evaluation of our approaches and also analyze their performance analytically.
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.