02141 Computer Science Modelling (Spring
2018)
Class schedule: Lectures and exercise classes generally take place Tuesday
13.00-17.00 and Friday 8.00-12.00 during the Spring Term.
Lectures and Exercises will both be in
303A-A041.
Course work: There is is a series of mandatory assignments – on
top of the exercises in class.
Examination: There is an individual written exam at the end of the
course; it may build in part on the mandatory assignments.
Rexamination: Reexaminations will be oral and individual; they may build in part on the
mandatory assignments.
Lecturers: Hanne Riis Nielson | email, Flemming Nielson | email, and Alberto Lluch Lafuente | email.
Tutors: Mike Castro Lundin and Martin
Obel Thomsen.
Getting help: Ask the tutors (and lecturer) during class; we will be
announcing when we have set up piazza
for general questions and for help between classes.
General course
objectives: The students learn
to understand and apply the central models and formalisms introduced in the
course and to use software tools related to some of these formalisms.
Course prerequisites: Please note that the course 02157 is a prerequisite for
this course, and we will be assuming that you can program in a functional
language like F#.
Course contents: The course covers three main topics:
Tentative teaching schedule: Please note that the following schedule is tentative
and may be changed.
WeekDay |
Date |
Meeting |
Topic |
Lecturer |
Description |
Reading material |
Tuesday |
30-Jan |
1 |
RL-1 |
HRN |
Introduction to Computer
Science Modelling |
HMU sec 1.1, 1.5,
2.1 |
Friday |
02-Feb |
2 |
RL-2 |
HRN |
Finite Automata |
HMU sec 1.4, 2.2, 2.3 |
Tuesday |
06-Feb |
3 |
FM-1 |
FN |
Program Graphs |
Why Formal Methods FM sec 1.1, 1.2, 1.3 |
Friday |
09-Feb |
4 |
RL-3 |
HRN |
Regular Expressions |
HMU sec 3.1, 3.2,
3.4 |
Tuesday |
13-Feb |
5 |
FM-2 |
FN |
Guarded Commands |
FM sec 2.1, 2.2, 2.3 |
Friday |
16-Feb |
6 |
RL-4 |
HRN |
Equivalence Results for
Regular Languages |
HMU sec 2.3, 2.5, 3.2 |
Tuesday |
20-Feb |
7 |
FM-3 |
FN |
Program Verification |
FM sec 3.1, 3.2, 3.3 |
Friday |
23-Feb |
8 |
RL-5 |
HRN |
Properties of Regular
Languages |
HMU sec 4.1, 4.2, 4.3 |
Tuesday |
27-Feb |
9 |
FM-4 |
FN |
Consolidation |
FM sec 1.4, 2.4, (2.5),
(3.4) |
Friday |
02-Mar |
10 |
CFL-1 |
ALL |
Parsing 1 |
HMU chap 5 |
Tuesday |
06-Mar |
11 |
CFL-2 |
ALL |
Parsing 2 |
HMU chap 5 |
Friday |
09-Mar |
12 |
CFL-3 |
ALL |
Parsing 3 |
HMU chap 5 |
Tuesday |
13-Mar |
13 |
FM-5 |
FN |
Program Analysis |
FM sec 4.1 4.2 4.3 |
Friday |
16-Mar |
14 |
MA-1 |
ALL |
Mandatory Assignment:
Parsing |
- |
Tuesday |
20-Mar |
15 |
FM-6 |
FN |
Program Analysis |
FM sec 4.4 4.5 |
Friday |
23-Mar |
16 |
CFL-4 |
ALL |
Compiling |
? |
Tuesday |
03-Apr |
17 |
FM-7 |
FN |
Language Based Security |
FM sec 5.1, 5.2, 5.3,
(5.4) |
Friday |
06-Apr |
18 |
MA-2 |
ALL |
Mandatory Assignment:
Compiling |
- |
Tuesday |
10-Apr |
19 |
FM-8 |
FN |
Model Checking |
FM sec 6.1, 6.2, 6.3, 6.4 |
Friday |
13-Apr |
20 |
CFL-5 |
ALL |
Push Down Automata |
HMU chap 6 |
Tuesday |
17-Apr |
21 |
FM-9 |
FN |
Concurrency |
FM sec 8.1, 8.2, 8.3 |
Friday |
20-Apr |
22 |
MA-3 |
ALL |
Mandatory Assignment: Interpreter |
- |
Tuesday |
24-Apr |
23 |
CFL-6 |
ALL |
Properties of Context Free Languages |
HMU chap 7 |
Tuesday |
01-May |
24 |
FM-10 |
FN |
Consolidation |
FM |
Friday |
04-May |
25 |
MA-4 |
ALL |
Mandatory Assignment: Analysis |
- |
Tuesday |
08-May |
26 |
Friday Schedule |
FN |
Wrapping up Computer Science Modelling |
Undecidability and Uncomputability |
Tentative
schedule for mandatory assignments:
Learning objectives: A student who has met the objectives of the course
will be able to:
Course literature:
Remarks: The course is given in English.
CampusNet:
https://cn.inside.dtu.dk/cnnet/element/562353/frontpage