Mecanización de verificación formal de programas en Dafny
Loading...
Date
2024
Publisher
Universidad ORT Uruguay
DOI
ISSN
ISBN
Abstract
El siguiente proyecto presenta un generador de condiciones de verificación que se ha desarrollado en Dafny, diseñado para un pequeño lenguaje imperativo. Este lenguaje incluye características como asignación múltiple, secuenciación, selección e iteración. El propósito fundamental de este generador es derivar, a partir de un programa anotado con pre y post condiciones, así como invariantes de cada iteración, un árbol de Hoare y condiciones de verificación asociadas. Se destaca que si las condiciones son demostradas, el programa resulta parcialmente correcto respecto a las pre y post condiciones dadas. Asimismo, se verifica que todo el programa compiló correctamente.
En
Thesis note
Proyecto (Carrera Universitaria). Universidad ORT Uruguay, Facultad de Ingeniería
Thesis degree name
Ingeniero en Sistemas
36 p.
Notes
Incluye bibliografía.
Subject
PROYECTOS-ID, LENGUAJES DE PROGRAMACIÓN-DAFNY, VERIFICACIÓN AUTOMÁTICA, MÉTODOS FORMALES
Type
Trabajo final de carrera
Access the full text
Citation
Colina Candiota, C. S. & Armas Baison, G. de (2024). Mecanización de verificación formal de programas en Dafny (Proyecto) Universidad ORT Uruguay, Facultad de Ingeniería. Recuperado de https://rad.ort.edu.uy/handle/20.500.11968/6957