Paper Info
Title
Experiences and new alternatives for teaching formal verification of Java programs.
Abstract
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.
Year
DOI
Venue
2018
10.1145/3197091.3205811
ITiCSE
Keywords
Field
DocType
Formal verification of algorithms, Hoare logic, Java, Krakatoa
Programming language,Axiom,Computer science,Correctness,Automated theorem proving,Hoare logic,Java,Multimedia,Formal verification
Conference
ISBN
Citations 
PageRank 
978-1-4503-5707-4
0
0.34
References 
Authors
1
2
Name
Order
Citations
PageRank
Ana Romero183.76
Jose Divasón2289.96