PhD Reading Group - Introductory Formal Methods

November 15 (2021) - February 7 (2022)

Organizers:

Dr. Mahsa Varshosaz (mahv@itu.dk)
Prof. Andrzej Wąsowski (wasowski@itu.dk)

Lecturers:

Prof. Erika Abraham, RWTH Aachen University (abraham@informatik.rwth-aachen.de)
Prof. Einar Broch Johnsen, University of Oslo (einarj@ifi.uio.no)
Dr. Silvia Lizeth Tapia Tarifa, University of Oslo (sltarifa@ifi.uio.no)
Dr. Mahsa Varshosaz, IT University of Copenhagen (mahv@itu.dk)
Prof. Andrzej Wąsowski, IT University of Copenhagen (wasowski@itu.dk)

Course advertisement:

Reading group page: https://remaro.eu/index.php/2021/10/15/reading-group-on-introductory-formal-methods/

Dates of the course:

15/11-2021 from 11:00-12:00
22/11-2021 from 11:00-12:00
29/11-2021 from 11:00-12:00
06/12-2021 from 11:00-12:00
13/12-2021 from 11:00-12:00
20/12-2021 from 11:00-12:00
17/01-2022 from 10:00-11:00
24/01-2022 from 11:00-12:00
31/01-2022 from 11:00-12:00
07/02/2022 from 11:00-12:00

Where:

Place at ITU will be announced in the website/Online

Course description:

The aim of the reading group is to critically engage with Formal Methods. We will start reading the book: Logic in Computer Science by Michael Huth and Mark Ryan, 2nd Edition. The readings cover fundamental topics such as propositional logic, predicate logic, temporal logic and the basics of model checking and program verification. The meetings will take place on a weekly basis at the IT University of Copenhagen and Virtually. Participants from all disciplinary backgrounds with an interest in Formal Methods are welcome to join the reading group. The Reading covers about 60% of the topics of the book. After the course, the students should be able to explain and discuss basic formal methods concepts, build formal models, and follow and create proofs of simple theorems.

Programme:

Programme

This reading group will be held in the form of a discussion group; first a chapter is presented collaboratively by lecturers and students in an hour introduction session followed by another session the week after in which all participants will continue with a thorough discussion on the chapter for an hour.

The discussion is led by a student.

15/11-2021 from 11:00-12:00 (Topic: Propositional Logic, Lecturer: Prof. Erika Abraham)
22/11-2021 from 11:00-12:00 (Topic: Propositional Logic)
29/11-2021 from 11:00-12:00 (Topic: Predicate Logic, Lecturer: Prof. Andrzej Wąsowski)
06/12-2021 from 11:00-12:00 (Topic:Predicate Logic)
13/12-2021 11:00-12:00 (Topic: Verification by Model Checking including Temporal Logics, lecturer:
Dr. Mahsa Varshosaz)
20/12-2021 from 11:00-12:00 (Topic: Verification by Model Checking including Temporal Logics)
17/01-2022 from 10:00-11:00, (Topic: Program Verification, Lectures: Prof. Einar Broch Johnsen, Dr.
Silvia Lizeth Tapia Tarifa)
24/01-2022 from 11:00-12:00, (Topic: Program Verification)
31/01-2022 from 11:00-12:00, (Topic: Binary Decision Diagrams, Lecturer: Prof. Erika Abraham)
07/02/2022 from 11:00-12:00, (Topic: Binary Decision Diagrams)

Reading list:

Logic in Computer Science by Michael Huth and Mark Ryan, 2nd Edition (about 300 pages).

Prerequisites:

None.

Exam:

Each student should lead a discussion or an introduction session at least once.

Credits:

The course is eligible for 2.5 ECTS.

Amount of hours the student is expected to use on the course:

Participation: one hour per meeting
Preparation: six hours per meeting (+ three hours of extra time when preparing a presentation)

How to sign up:

Each participant must submit an overview (up to one page) of their doctoral
research that describes their research question and expected contributions.
Email to mahv@itu.dk.

Deadline for signing-up 07/11-2021.