Trabajo Fin de Máster
Verificación formal de la lógica de Hoare en Isabelle/HOL
Autor/es | González Blanco, Natividad |
Director | Hidalgo Doblado, María José |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2016-09 |
Fecha de depósito | 2016-10-26 |
Titulación | Universidad de Sevilla. Máster Universitario en Matemáticas |
Resumen | 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 ... 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. |
Cita | 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. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
González Blanco Natividad TFM.pdf | 745.0Kb | [PDF] | Ver/ | |