Formal Derivation of Algorithm and Isabelle-based Automatic Verification
The continuous development of trustworthy software promotes the in-depth study of formal methods.This paper focuses on the formal derivation of algorithm based on recurrence relations.We show two examples of automated transformation processes by combining Isabelle theorem prover with Dijkstra weakest precondition method,that can avoid the error-prone and long-winded problems in manual verification processes.The algorithm formal method that based on recursive relationship can make the derivation process correct through mathematical transformation to ensure the correctness of the algorithm program,as the paper shows.
Formal methods Isabelle theorem prover automatic verification formal derivation
Qinghong Yang Leilei Qi Ying You
College of Computer Information Engineering,Jiangxi Normal University Nanchang,China
国际会议
重庆
英文
361-365
2017-03-25（万方平台首次上网日期，不代表论文的发表时间）