CISTER-ISEP MScCCSE 2021/2022

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

**Real-time models**- Timed Automata and Hybrid Automata
- Temporal logic
- Static verification using UPPAAL

**Program verification**- First Order Logic Revisited
- Abstract Program Semantics
- Design by Contract and Hoare Logic
- Verification of annotated programs

**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)
- TP3: Implementation of a Simple Program Verifier using Hoare Logic

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

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