Verificación formal de la lógica de Hoare en Isabelle/HOL

Abstract

Hoare logic is a formal system developed by C.A.R. Hoare. This logic was introduced to verify formally imperative programs. That is, with the Hoare logic we can ensure and prove that a particular program performs exactly the actions for which it has been designed. An advantage to do it through a proof assistant is that in this way errors can be detected that in the handmade proofs could go unnoticed. In this dissertation, we will describe briefly the interactive theorem prover Isabelle/HOL. Then, we will present in detail the Hoare logic with examples. The major goal consists of an implementation of this logic in the proof assistant Isabelle/HOL. According as the size of a system grows, the costs of formal verification increase disproportionately. So some people think that formal verification isn’t very profitable but there are some situations in which this is vitally important such as braking systems of cars and aircraft piloting by electronic controls.