Formal Methods in Software Development 26230
- Centre
- Faculty of Informatics
- Degree
- Bachelor's Degree in Informatics Engineering
- Academic course
- 2024/25
- Academic year
- 4
- No. of credits
- 6
- Languages
- Spanish
- Code
- 26230
TeachingToggle Navigation
Teaching guideToggle Navigation
Description and Contextualization of the SubjectToggle Navigation
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.
Skills/Learning outcomes of the subjectToggle Navigation
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.
Theoretical and practical contentToggle Navigation
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
MethodologyToggle Navigation
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.
Assessment systemsToggle Navigation
- Continuous Assessment System
- Final Assessment System
- Tools and qualification percentages:
- Individual works (%): 100
Ordinary Call: Orientations and DisclaimerToggle Navigation
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.
Extraordinary Call: Orientations and DisclaimerToggle Navigation
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.
Compulsory materialsToggle Navigation
- Lectures slides.
- The on-line tutorial and the documentation of the Web page: https://dafny.org/
BibliographyToggle Navigation
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
GroupsToggle Navigation
16 Teórico (Spanish - Tarde)Show/hide subpages
Weeks | Monday | Tuesday | Wednesday | Thursday | Friday |
---|---|---|---|---|---|
16-30 | 14:00-15:30 (1) | 15:30-17:00 (2) |
Teaching staff
16 Applied laboratory-based groups-1 (Spanish - Tarde)Show/hide subpages
Weeks | Monday | Tuesday | Wednesday | Thursday | Friday |
---|---|---|---|---|---|
16-30 | 17:00-18:30 (1) |