This course teaches the main principles of Formal Verification of Software, with specific focus on applications that can be characterized as being critical computing applications.

1. Mathematical Foundations

• Preliminaries:
  • Set Theory
  • Transition Systems
• Propositional and First-Order logics:
  • Syntax and Semantics
  • Natural Deduction
  • Automated Theorem Proving (SAT & SMT solving)

2. Program Semantics

• Small Step and Big Step Operational Semantics
• Hoare Logic's axiomatic semantics

3. Reasoning over Programs

• SAT and SMT solvers
• Automatic theorem proving using Z3
• Introduction to Interactive theorem proving using Coq

• 0. Introduction
• 1. Modelling with Timed Automata
• 2. Verification of Timed Automata
• 3. A Not So Formal Introduction to Formal Verification of Program Code
• 4. Operational Semantics
• 5. Hoare Logic.pdf
• 6. Hoare Logic and Verification Condition Generation I
• 7. Hoare Logic and Verification Condition Generation II
• 8. Hoare Logic and Verification Condition Generation III
• ...

• TP1: Specification and Verification in Uppaal (group)
• TP2: Exercises about Hoare Logic and Verification Conditions Generation (not subject to evaluation)

• Final mark = Project (60%) + Exam (40%)

The project will be performed in groups of 2 students, addressing the practical aspects involving model checking and theorem proving, and will include some homework exercises. The exam will evaluate the student’s knowledge on the theoretical aspects.

Homework consists of a PDF report that must be submitted until Sunday @ 23:59 of the following week of being shown during lessons. For example, all exercises presented in the slides used in the week 8 Nov - 12 Nov must be submitted until Sunday 21 Nov. Assignments have specific deadlines, mentioned on their instructions. The deadlines are summarised below, and may still suffer changes.

• 20 Mar (Sun) @ 23:59 - Slides 1 (pages 1-37)
• 27 Mar (Sun) @ 23:59 - Slides 1 (pages 37-end); Slides 2 (pages 1-19 except 8)
• 3 Apr (Sun) @ 23:59 - Slides 2 (pages 8 and 20-end)
• 8 May (Sun) @ 23:59 (extended) - TP1: Specification and verification in Uppaal

• David Pereira, drp arroba isep ponto ipp ponto pt
• José Proença, pro arroba isep ponto ipp ponto pt
• Eduardo Tovar, emt arroba isep ponto ipp ponto pt

We will use a team in Microsoft Teams where all questions regarding this course unit should be placed, and where we can schedule virtual meetings if needed.