Formal methods make software development acquire a more scientific character and similar to other disciplines related to engineering, as well as promote the use of tools with solid foundations, as occurs in other well-established disciplines. These methods are called formal because they are based on mathematics, mainly on mathematical logic. Some years ago the industrial development of system using formal techniques was considered a complex theoretical exercise and unfeasible in real problems. However, the increasing complexity and importance of the computer systems ended up making patent the importance of construct reliable and safe systems, i.e. systems that lack errors or failures. Not only because of the terrible repercussions these failures can have in areas where security is critical, but also because of the economic and quality repercussions that affect companies. This, together with the fact that computer systems play an increasingly essential role in society (in particular, they are more and more present in the devices that we use every day) made the industrial world change its attitude. Thus, in the last decades, formal methods have gained a notable advance and their use in the industrial field has ceased to be the utopia that their detractors claimed. Currently there are large companies, such as Intel, IBM, Sony, Siemens, Amazon or Microsoft, which collaborate very actively both in the creation of tools to help formal software development, and in the application of these tools to obtain reliable industrial applications. In fact, this course uses a software development tool created by Microsoft: Dafny. Although the usefulness of formal methods, and their efficiency, in industrial developments are already proved, more work is still needed for most engineers to know and apply them. This work must be carried out by the universities that must include them in their academic content; by the teachers, who must be trained and researched in this area of knowledge; and by the students, who must have a more solid formation in mathematics and logic. This course contributes to this task of ensuring that the software engineer's work is true engineering, so that the end user receives reliable and safe products.

The specific objectives of this subject are:

- Understand the importance of programming being a more scientific than craft activity.

- Know the history and motivation of formal methods of software development.

- Know the state of the art in the area of formal software development.

- Know the languages, methods and concrete tools of formal software development.

- Ability to handle languages and concrete tools of formal software development.

Topic 1.- Introduction

Topic 2.- Mathematical Induction

Topic 3.- Introduction to the Dafny System

Topic 4.- Value Types

Topic 5.- Structural Induction and Datatypes

Topic 6.- Arrays and Framing

Topic 7.- Modules and Objects

We use different teaching metodologies. In classes, the conceptual contents of the subject will be presented and in the laboratories, practical problems will be solved using the Dafny tool, in an interactive way, in which the students use the tool at the same time as the teacher. Problems and exercises will be provided that students must develop individually, so that they can be aware of their learning level throughout the semester.

• Continuous Assessment System
• Final Assessment System
• Tools and qualification percentages:
  • Individual works (%): 100

In order to pass the subject in continuous assessment, students must carry out three individual practical assignments in the laboratory that test their knowledge of the tools and techniques addressed in class. The percentage of the grade for each practical work is 30% for the first, 40% for the second and 30% for the third.

The global evaluation consists of carrying out individual practical work in the laboratory that is equivalent to the set of works carried out during the course for continuous evaluation.

- Lectures slides.

- The on-line tutorial and the documentation of the Web page: https://dafny.org/

Basic bibliography

- Documentación de la página Web:

https://dafny.org/



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

In-depth bibliography

- 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)

Journals

- 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

Web addresses

- Dafny: a language and program verifier for functional correctness
https://dafny.org/

- Formal Methods and Software Technology - Interesting Conferences
http://user.it.uu.se/~bengt/Info/conferences.shtml