Los objetivos concretos de esta asignatura son:

- Entender la importancia de que la programación sea una actividad más científica que artesanal.

- Conocer la historia y motivación de los métodos formales de desarrollo de software.

- Conocer el estado del arte del área del desarrollo formal de software.

- Conocer lenguajes, métodos y herramientas concretos de desarrollo formal de software.

- Capacidad para manejar lenguajes y herramientas concretas de desarrollo formal de software.

Tema 1.- Introducción

Tema 2.- Inducción matemática

Tema 3.- Introducción al lenguaje y verificador Dafny

Tema 4.- Generación de condiciones de verificación

Tema 5.- Tipos de valores

Tema 6.- Inducción Estructural y Datatypes

Tema 7.- Arrays y Framing

En esta asignatura se utilizan diversas metodologías de enseñanza. Se impartirán tanto clases de exposición de los contenidos conceptuales de la materia, como laboratorios de resolución de problemas prácticos utilizando la herramienta Dafny, de forma interactiva, en la que los/las estudiantes utilizan la herramienta a la vez que la profesora. Se proporcionarán problemas y ejercicios que los/las estudiantes deberán desarrollar individualmente. Para facilitar y asegurar el aprendizaje del alumnado, se hará un seguimiento tanto de las prácticas de aula como de las de ordenador. Se proporcionará un detallado feed-back de todos los ejercicios planteados y en especial de los que sirven para la evaluación continua, de manera que los y las estudiantes puedan ser conscientes de su nivel de aprendizaje a lo largo del cuatrimestre.

Para superar la asignatura en evaluación continua los/las estudiantes deberán realizar en el laboratorio varios trabajos prácticos individuales que prueben su conocimiento de las herramientas y técnicas que abordadas en clase. Los/Las estudiantes recibirán feedback sobre dichos trabajos a medida que la profesora los vaya corrigiendo, de modo que resulten útiles para el aprendizaje.

- Transparencias de clase.

- El tutorial on-line y la documentación de la página Web:
https://dafny.org/

Bibliografía básica

- Documentación de la página Web:

https://dafny.org/

Bibliografía de profundización

- K. Rustan M. Leino. Program Proofs. MIT Press, March 2023. ISBN 9780262546232

- Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald.
Formal methods: Practice and Experience.
ACM Computing Surveys, 41(4):19:1–19:36, October 2009.

- Jason Koenig and K. Rustan M. Leino. Getting started with Dafny: a guide. In Marktoberdorf 2011 lecture notes. (http://research.microsoft.com/en-us/um/people/leino/papers/krml220.pdf)

- K. Rustan M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR-16, volume 6355 of LNCS, pages 348-370. Springer, 2010. (http://research.microsoft.com/en-us/um/people/leino/papers/krml203.pdf)

- Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Incorporated, 1976, ISBN 0-613-92411-8

Revistas

- ACM Transactions on Computational Logic
- ACM Transactions on Software Engineering and Methodology
- Applicable Algebra in Engineering, Communication and Computing.
- Formal Aspects of Computing
- Formal Methods in System Design
- Journal of Automated Reasoning
- Software Testing Verification & Reliability