In recent years and decades, the research community has unleashed a diverse variety of approaches to formally assess and establish the correctness of programs on the source code level. It is still an active research area how the results of different verification techniques can be brought together profitably.

In this talk, I will present how the verification ecosystem surrounding the KeY tool allows one to combine a number of successful approaches. At its core, KeY is a deductive verification engine for the formal analysis of Java programs annotated with formal specifications written in the Java Modeling Language. It employs a dynamic logic calculus for Java driven by symbolic execution. We will learn about the working principles of this verification method and see how it was used to prove (or disprove) the correctness of relevant real-world Java components, for instance from the JDK.

In addition, I will present the Karlsruhe Java Verification Suite (KaJaVe), where we enriched the KeY prover infrastructure by a number of approaches that leverage other verification principles such that they can be used in combination with the deductive verifier.