Formal Verification of Critical Applications (FVOCA)



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



Exercises and Assignments



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.


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.