Experiences and new alternatives for teaching formal verification of Java programs
Ana Romero, Jose Divasón · 2018
Formal verification of algorithms is traditionally taught in Computer Science studies in a theoretical way by means of the Hoare logic axioms and doing (by hand) exercises of verification of small programs. This work shows our experience with Krakatoa, an automatic theorem prover which allows students to interactively visualize the steps required to prove the correctness of a program.