FVOCA - Formal Verification of Critical Applications

Course structure

This course teaches the basic principles of Model-Driven Engineering - MDE. Students should learn:

1. Real-time models
   • Timed Automata and Hybrid Automata
   • Temporal logic
   • Static verification using UPPAAL
2. Program verification
   • First Order Logic Revisited
   • Abstract Program Semantics
   • Design by Contract and Hoare Logic
   • Verification of annotated programs
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)
• TP3: Implementation of a Simple Program Verifier using Hoare Logic

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
• 12 Jun (Sun) @ 23:59 - TP3: Implementation of a Simple Program Verifier using Hoare Logic

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.