Formal Verification of Critical Applications (FVOCA)

Logo

CISTER-ISEP MScCCSE 2021/2022

View the Project on GitHub cister-labs/fvoca2122

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

Exercises and Assignments

Pragmatics

Evaluation

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.

Lecturers

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.