Abstract

Writing the correctness proof of a programme in Hoare Logic is both tedious and error-prone. But programme verification, such as Hoare logic, is important. If it is not used, many computer programmes could be faulty. To lower the frustration of the learning process of Hoare logic and help with a better understanding of programme verification, we made a proof checker that will make this process easier and faster. We use an SMT checker and translate Hoare logic to SMT and interpret the answers from it back to Hoare logic. The prototype of this tool can handle most standard operators. This tool differs from it is competitors in that it gives enough feedback to pinpoint the problem but not spoil the learning process.

Additional Resources

1. The paper