FVOCA - Formal Verification of Critical Applications

Course structure

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

Material

Slides

• 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
• ...

Exercises and Assignments

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

Pragmatics

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.

Deadlines

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

Lecturers

• 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.