02141 Computer Science Modelling (Spring 2017)

 

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 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, Hugo-André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 Context-Free Languages

HMU sec 5.1, 5.2

10/3

12

FM

FN

Verification

FM chap 3

14/3

13

CFL

ALL

Using Context-Free 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.1-6.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 Context-Free Languages

HMU sec 7.1-7.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