A Survey of Verification Tools Based on Hoare Logic
Nahid A. Ali · International Journal of Software Engineering & Applications · 2017
The quality and the correctness of software has a great concern in computer systems.Formal verification tools can used to provide a confidence that a software design is free from certain errors.This paper surveys tools that accomplish automatic software verification to detect programming errors or prove their absence.The two tools considered are tools that based on Hoare logic namely, the KeY-Hoare and Hoare Advanced Homework Assistant (HAHA).A detailed example on these tools is provided, underlining their differences when applied to practical problems.