Admission requirements
Students are expected to have computer science knowledge at the BSc level, including basic familiarity with logic and formal reasoning. Prior coursework in verification, testing, or related topics is recommended, for example Programmeren & Correctheid or Theory of Concurrency.
This is an advanced course. Students will engage with current research topics and recent developments in formal methods and trustworthy AI.
Description
Intelligent autonomous systems are increasingly deployed in a wide range of domains, driven by advances in modelling, sensing, learning, and algorithm design. With the rapid development of such systems, there is a growing need to ensure that they are correct, safe, reliable, and trustworthy. Formal methods provide rigorous techniques for analysing and assuring such systems.
This course explores the intersection of formal methods and artificial intelligence.
The course begins with a short sequence of introductory lectures, readings, and homework assignments that introduce important techniques in formal methods, including SAT and SMT solving, model checking, runtime monitoring, and shielding. The remainder of the course is centred around reading and discussing recent research papers. Students will take turns presenting papers and leading discussions. In parallel, students will work in groups of 2–3 on a research project that runs throughout the course. The project gives students the opportunity to investigate a current research topic in depth and to apply the techniques discussed in class. The course will also include guest lectures by leading experts in the field.
Course objectives
By the end of the course, students will be able to:
explain the role of formal methods in the analysis and assurance of intelligent and autonomous systems;
describe and compare state-of-the-art techniques such as SAT/SMT solving, model checking, monitoring, and shielding;
read, analyse, and critically discuss scientific papers in formal methods and AI;
identify the main ideas, assumptions, limitations, and contributions of a research paper;
present technical material clearly, both orally and in writing;
formulate a research question related to formal methods and intelligent systems;
carry out a research project in a team;
apply formal methods tools/techniques to a concrete problem;
interpret experimental results and evaluate the strengths and limitations of a proposed approach;
collaborate effectively in a research setting and communicate research findings.
Schedule
The most recent timetable can be found at the Computer Science (MSc) student website.
In MyTimetable; you can find all course and programme schedules; allowing you to create your personal timetable. Activities for which you have enrolled via MyStudyMap will automatically appear in your timetable.
Additionally; you can easily link MyTimetable to a calendar app on your phone; and schedule changes will be automatically updated in your calendar. You can also choose to receive email notifications about schedule changes. You can enable notifications in Settings after logging in.
Questions? Watch the video; read the instructions; or contact the ISSC helpdesk.
Note: Joint Degree students from Leiden/Delft need to combine information from both the Leiden and Delft MyTimetables to see a complete schedule. This video explains how to do it.
Teaching method
lectures;
readings;
homework assignments;
paper presentations and discussions;
collaborative project work.
Assesment method
Overall, the course is assessed based on homework, paper summaries, a paper presentation, and a project. The course project forms the largest component of the final grade. Homework assignments are intended to familiarize students with formal methods tools and techniques in preparation for the project. In addition, each student will read, summarize, present, and discuss technical research papers.
The final grade is composed as follows:
10% homework assignments (individual)
20% paper summaries and presentation
20% participation
50% course project
The project grade will be adjusted within each team to reflect the individual contributions of the team members.
To pass the course, each individual grade has to be at least 5.5, and students must attend at least 80% of the lectures.
Resit, review & feedback
Students who do not obtain a passing grade for one or more course components may resit only the failed components. Homework assignments may be replaced by an additional individual assignment. The paper summary and presentation, as well as the participation components may be resat through an additional written summary and oral presentation of a research paper. Students who do not pass the course project may submit a revised version of the project report.
Reading list
The reading list changes each year to reflect recent developments in formal methods and trustworthy AI. Further information will be provided on the Brightspace course page.
Registration
As a student; you are responsible for enrolling on time through MyStudyMap.
In this short video; you can see step-by-step how to enrol for courses in MyStudyMap.
Extensive information about the operation of MyStudyMap can be found here.
There are two enrolment periods per year:
Enrolment for the fall opens in July
Enrolment for the spring opens in December
See this page for more information about deadlines and enrolling for courses and exams.
Note:
It is mandatory to enrol for all activities of a course that you are going to follow.
Your enrolment is only complete when you submit your course planning in the ‘Ready for enrolment’ tab by clicking ‘Send’.
Not being enrolled for an exam/resit means that you are not allowed to participate in the exam/resit.
Contact
Lecturer: [dr. Emily Yu]
Remarks
This course is also suitable for, and recommended to, PhD students who wish to apply formal methods in their own research projects.