Repositorio de producción científica de la Universidad de Sevilla

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


Advanced Search
Opened Access Verificación formal de la lógica de Hoare en Isabelle/HOL
Show item statistics
Export to
Author: González Blanco, Natividad
Director: Hidalgo Doblado, María José
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2016-09
Document type: Master's Thesis
Academic Title: Universidad de Sevilla. Máster Universitario en Matemáticas
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.
Cite: González Blanco, N. (2016). Verificación formal de la lógica de Hoare en Isabelle/HOL. (Trabajo fin de master inédito). Universidad de Sevilla, Sevilla.
Size: 745.0Kb
Format: PDF


This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)