STAF 2023
Tue 18 - Fri 21 July 2023 Leicester, United Kingdom
Wed 19 Jul 2023 13:45 - 15:15 at Willow - TAP Session 5: Keynote Chair(s): Virgile Prevosto

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.

Wed 19 Jul

Displayed time zone: London change

13:45 - 15:15
TAP Session 5: KeynoteKeynotes at Willow
Chair(s): Virgile Prevosto CEA Tech List

Remote Participants: Zoom Link

KeY: A Verification Platform For Java