02141 Computer Science Modelling (Spring
2017)
Class schedule: Lectures and exercise classes generally take place Tuesday
13.0017.00 and Friday 8.0012.00 during the Spring Term. Lectures and
Exercises will both be in 303AA041.
Course work: There are three mandatory assignments, one in each of
the three topics of the course, on top of the exercises.
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.
Lecturers: Hanne Riis
Nielson  email,
Alberto Lluch Lafuente  email, Flemming Nielson  email, and Jan Midtgaard  email.
Tutors: Andreas Viktor Hess, HugoAndrés López, Kasper Laursen.
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 contents: The course covers three main topics:
Tentative teaching schedule (more details
later): Please note that we will be
reorganizing the teaching schedule and course contents with respect to 2016.
Date

Meeting 
Topic 
Lecturer 
Description

Reading material

31/1 
1 
RL 
HRN 
Introduction
to Computer Science Modelling 
HMU
sec 1.1, 1.5, 2.1 
3/2 
2 
RL 
HRN 
Finite
Automata 
HMU
sec 1.4, 2.2, 2.3 
7/2 
3 
RL 
HRN 
Regular
Expressions 
HMU
sec 3.1, 3.2, 3.4 
10/2 
4 
RL 
HRN 
Equivalence
Results for Regular Languages 
HMU
sec 2.3, 2.5, 3.2 
14/2 
5 
RL 
HRN 
Properties
of Regular Languages 
HMU
sec 4.1, 4.2 
17/2 
6 
FM 
FN 
Program
Graphs 
FM
chap 1 
21/2 
7 
RL 
HRN 
Decision
Procedures for Regular Languages 
HMU
sec 4.3, 4.4 
24/2 
8 
FM 
FN 
Guarded
Commands 
FM
chap 2 
28/2 
9 
RL 
(HRN) 
Assignment on Regular Languages 
N/A 
3/3 
10 
FM 
FN 
Model
Checking 
FM
chap 5 
7/3 
11 
CFL 
ALL 
Introduction
to ContextFree Languages 
HMU
sec 5.1, 5.2 
10/3 
12 
FM 
FN 
Verification

FM
chap 3 
14/3 
13 
CFL 
ALL 
Using
ContextFree Grammars 
HMU
sec 5.3, 5.4 
17/3 
14 
FM 
FN 
Program
Analysis 
FM
chap 4 
21/3 
15 
CFL 
ALL 
Using
Parser Generators 
(Material
on ANTLR) 
24/3 
16 
FM 
(FN) 
Assignment on Semantics and Analysis 
N/A 
28/3 
17 
CFL 
ALL 
Pushdown
Automata 
HMU
sec 6.16.3 
31/3 
18 
SwA 
FN 
Natural
Semantics 
SwA sec 1.2, 1.3, 1.4, 2.1 
4/4 
19 
CFL 
ALL 
Deterministic
Pushdown Automata 
HMU
sec 6.4 
7/4 
20 
SwA 
FN 
Structural
Operational Semantics 
SwA sec 2.2, 2.3 
18/4 
21 
CFL 
ALL 
Properties
of ContextFree Languages 
HMU
sec 7.17.4 
21/4 
22 
SwA 
FN 
More on Operational Semantics 
SwA sec 3.1, app A 
25/4 
23 
CFL 
(ALL) 
Assignment on Context Free Languages 
N/A 
28/4 
24 
SwA 
JM 
Provably Correct Implementation 
SwA sec 4.1, 4.2 
2/5 
25 
FM 
FN 
Language Based Security 
FM
chap 6 
5/5 
26 
N/A 
FN 
Wrapping Up 
N/A 
Tentative
schedule for mandatory exercises:
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/536873