Master's Final Project
Verificación formal de la lógica de Hoare en Isabelle/HOL
dc.contributor.advisor | Hidalgo Doblado, María José | es |
dc.creator | González Blanco, Natividad | es |
dc.date.accessioned | 2016-10-26T10:11:12Z | |
dc.date.available | 2016-10-26T10:11:12Z | |
dc.date.issued | 2016-09 | |
dc.identifier.citation | 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. | |
dc.identifier.uri | http://hdl.handle.net/11441/48170 | |
dc.description.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. | es |
dc.format | application/pdf | es |
dc.language.iso | spa | es |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Verificación formal de la lógica de Hoare en Isabelle/HOL | es |
dc.type | info:eu-repo/semantics/masterThesis | es |
dc.type.version | info:eu-repo/semantics/publishedVersion | es |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | es |
dc.contributor.affiliation | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial | es |
dc.description.degree | Universidad de Sevilla. Máster Universitario en Matemáticas | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Logica, Computacion e Ingenieria del Conocimiento | es |
idus.format.extent | 123 p. | es |
dc.identifier.idus | https://idus.us.es/xmlui/handle/11441/48170 |
Files | Size | Format | View | Description |
---|---|---|---|---|
González Blanco Natividad TFM.pdf | 745.0Kb | [PDF] | View/ | |