Formalization of graphs in Dafny
Loading...
Date
2024
Publisher
Universidad ORT Uruguay
DOI
ISSN
ISBN
Abstract
Dafny es un lenguaje orientado a especificaciones que provee un marco para verificar formalmente programas. En este proyecto, se presenta la experiencia de formalizar grafos y lograr la verificación parcial de algoritmos conocidos utilizando Dafny (Prim y Kruskal). En el cuerpo de este trabajo, también se presentan las pruebas de las secciones de los algoritmos que se verificaron, y cuales secciones fueron determinadas como trabajo a futuro. Se concluye que las especificaciones en Dafny son extremadamente poderosas si son bien ejecutadas, pero además requieren un conocimiento profundo de los algoritmos que se quiere especificar y de los problemas que resuelven, además de un manejo experto de Dafny para algoritmos complejos.
En
Thesis note
Proyecto (Carrera Universitaria). Universidad ORT Uruguay, Facultad de Ingeniería
Thesis degree name
Ingeniero en Sistemas
73 p. diagrs., tbls., grafs.
Notes
Incluye bibliografía y anexos.
Subject
PROYECTOS-ID, LENGUAJES DE PROGRAMACIÓN-DAFNY, TEORÍA DE GRAFOS, ALGORITMOS, VERIFICACIÓN FORMAL
Type
Trabajo final de carrera
Access the full text
Citation
Bordagorry Burgueño, J. M. & Pérez Pedetti, S. (2024). Formalization of graphs in Dafny (Proyecto). Universidad ORT Uruguay, Facultad de Ingeniería. Recuperado de https://rad.ort.edu.uy/handle/20.500.11968/6956