02141 Computer Science Modelling (Spring 2019)

 

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 358.060a.

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: Mathias Bøtcher Iversen,  Sébastien Pierre Christophe Gondron (only FM part),  Lasse Dissing Hansen (only MA part),  Snorre Christian Dam Clasen (only MA part).

Getting help: Ask the tutors and lecturer during class.

 

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:

• Regular Languages (RL): Regular languages and their relation to (deterministic and non-deterministic) finite automata, practical applications (searching in texts, lexical analysis, etc.) and some key theoretical properties (for example closure and decidability properties).
• Context-Free Languages (CFL): Context-free languages and their applications to parsing data and programs, and to the construction of interpreters and analyzers.
• Formal Methods (FM): Program graphs as a model of programs, their semantics, and several ways of analyzing and verifying properties of programs (including program analysis and language based security).

Tentative teaching schedule: Please note that the following schedule is tentative and may be changed.

WeekDay	Date	Meeting	Topic	Lecturer	Description	Reading material
Tuesday	5 Feb	1	RL-1	HRN	Introduction	HMU 1.1 1.5 2.1
Friday	8 Feb	2	RL-2	HRN	Finite Automata	HMU 1.4 2.2 2.3
Tuesday	12 Feb	3	RL-3	HRN	Regular Expressions	HMU 3.1 3.2 3.4
Friday	15 Feb	4	FM-1	FN	Formal Methods, Program Graphs	Quanta Magazine, FM 1.1-1.3
Tuesday	19 Feb	5	CFL-1	ALL	Introduction to Context Free Grammars	HMU 5.1 5.2
Friday	22 Feb	6	FM-2	FN	Guarded Commands	FM 2.1-2.3
Tuesday	26 Feb	7	CFL-2	ALL	Grammars and data, ambiguities, associativity and precedence	HMU 5.4
Friday	1 Mar	8	FM-3	FN	Program Graphs, Guarded Commands	FM 1.4 2.4 (2.5)
Tuesday	5 Mar	9	CFL-3	ALL	Parser Generators, abstract syntax and demo	HMU 5.3
Friday	8 Mar	10	MA-1	ALL	Parsing	*
Tuesday	12 Mar	11	CFL-4	ALL	Push Down Automata	HMU 6
Friday	15 Mar	12	MA-2	ALL	Compiling	*
Tuesday	19 Mar	13	FM-4	FN	Model Checking	FM 6.1-6.2
Friday	22 Mar	14	FM-5	FN	Model Checking	FM 6.3-6.4
Tuesday	26 Mar	15	RL-4	HRN	Equivalence Results for Regular Languages	HMU 2.3 2.5 3.2
Friday	29 Mar	16	MA-3	ALL	Interpreters	*
Tuesday	2 Apr	17	RL-5	HRN	Properties of Regular Languages	HMU 4.1 4.2 4.3
Friday	5 Apr	18	FM-6	FN	Program Analysis	FM 4.1-4.3
Tuesday	9 Apr	19	FM-7	FN	Program Analysis	FM 4.3-4.5
Friday	12 Apr	20	MA-4	ALL	Program Analysis	*
Tuesday	23 Apr	21	*	FN	Undecidability and Uncomputability	Lecture Notes
Friday	26 Apr	22	FM-8	FN	Language Based Security	FM 5.1-5.2
Tuesday	30 Apr	23	FM-9	FN	Language Based Security	FM 5.3-5.4
Friday	3 May	24	MA-5	ALL	Language Based Security	*
Tuesday	7 May	25	FM-10	FN	Concurrency	FM 8.1-8.2
Friday	10 May	26	*	ALL	Wrapping Up	*

 

Tentative schedule for mandatory assignments:

• MA-1 to be handed in before midnight on Thursday 14 March.
• MA-2 to be handed in before midnight on Thursday 28 March.
• MA-3 to be handed in before midnight on Thursday 4 April.
• MA-4 to be handed in before midnight on Thursday 25 April.
• MA-5 to be handed in before midnight on Thursday 9 May.

Learning objectives: A student who has met the objectives of the course will be able to:

• state the difference in expressive power of some of the formal models covered
• interpret the meaning of a given description in a formal model (e.g., automata, grammars, semantics)
• derive a description in a formal model (e.g., automata, grammars, semantics) of a desired property or behaviour given in a textual description
• translate into another model (e.g. regular expressions to NFA)
• modify a given description according to certain criteria (e.g. minimization of automata, removal of useless productions, adding language constructs)
• operate selected tools relating to the formal models (e.g., lexers, parsers)
• dectermine whether a description in a given formal model satisfies a given property
• derive properties using given proof strategies (e.g. structural induction, stated theorems)
• select formal models may be necessary or useful for a given problem
• achieve the goals as part of a group effort, while maintaining individual accountability
• communicate his or her constructions and solutions in a clear and precise manner

 

Course literature:

• [HMU] Introduction to Automata Theory, Languages, and Computation, John E. Hopcroft, Rajeev Motwani, Jefrey D. Ullman, Addison-Wesley, 2007. The chapters needed will be available from Polyteknisk Boghandel as 02141: Automata Theory and Languages. (The second edition ia801403.us.archive.org might also be used if you check for any changes in numbering of exercises etc.).
• [FM] Formal Methods – An Appetizer, Hanne Riis Nielson and Flemming Nielson. To appear, Springer, 2019. Has been ordered by Polyteknisk Boghandel but is delayed from the publisher; in the interim the version from last year is available on DTU Inside.
• Slides and additional notes will be made available on DTU Inside when appropriate.

 

Remarks: The course is taught in English.

 

DTU Inside: https://cn.inside.dtu.dk/cnnet/element/589255/frontpage