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.- Verification Conditions Generation

Topic 5.- Value Types

Topic 6.- Structural Induction and Datatypes

Topic 7.- Arrays and Framing

Various teaching methodologies are used in this subject. We use different teaching metodologies. Both classes will be taught to present the conceptual contents of the subject, as well as practical problem-solving laboratories 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 the students will have to develop individually. To facilitate and ensure student learning, both classroom and computer practices will be monitored. A detailed feedback will be provided on all the exercises proposed and especially those used for continuous assessment, so that students can be aware of their level of learning 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 several individual practical assignments in the laboratory that test their knowledge of the tools and techniques addressed in class. The students will receive feedback on these works as the teacher corrects them, so that they are useful for learning.



NOTE: In case of return to confinement, the evaluation tests (both continuous and final) will be carried out electronically through questionnaires, interviews and / or deliveries of eGela and through the BBC connection.

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.



NOTE: In case of return to confinement, the evaluation tests will be carried out electronically through questionnaires, interviews and / or deliveries of eGela and through the BBC connection.

- Lectures slides.
- The on-line tutorial and the documentation of the Web page:
http://research.microsoft.com/en-us/projects/dafny/

Basic bibliography

- The on-line tutorial and the documentation of the Web page:

http://research.microsoft.com/en-us/projects/dafny/

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)
- Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Incorporated, 1976, ISBN 0-613-92411-8
- Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996. ISBN 9780387945934

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
http://research.microsoft.com/en-us/projects/dafny/

- The Verification Corner (Microsoft Research):
http://research.microsoft.com/en-us/projects/verificationcorner/

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