Tags:automated theorem provers, Formal methods, Hoare logic, JML and Krakatoa
Abstract:
In this work, we present a study of different support tools to teach formal verification of Java programs and show our experience with Krakatoa, an automatic theorem prover based on Hoare logic which allows students to interactively visualize the different steps required to prove the correctness of a program, to think about the used reasoning and to understand the importance of verification of algorithms to improve the reliability of our programs.
Using Krakatoa for teaching formal verification of Java programs