Remco Swenker - Translating Hoare Logic To SMT, The Making Of A Proof Checker

author:Remco Swenker
title:Translating Hoare Logic To SMT, The Making Of A Proof Checker
keywords:Hoare logic, SMT solver
topics:Logics and semantics
committee:dr. S.C.C. Blom
prof.dr. M. Huisman
graduation date:25 June 2012


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.