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:

• Regular Languages: Regular languages and their relation to (deterministic and non-deterministic) finite automata, practical applications (searching in texts, lexical analysis, security automata, etc.) and some key theoretical properties (including closure and decidability properties).
• Context-Free Languages: Context-free languages and their applications (in parsing and XML documents) together with a brief introduction to pushdown automata and their relationship to context free languages.
• Semantics and Analysis: Transition systems and their applications in operational semantics for a variety of language constructs as well as formal techniques for reasoning about them.

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:

• On regular languages: 2/3 at 17.00.
• On semantics: 27/3 at 17.00.
• On context free languages: 27/4 at 17.00.

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. Both the second and third edition can be used. See https://www.pearsonhighered.com/program/Hopcroft-Introduction-to-Automata-Theory-Languages-and-Computation-3rd-Edition/PGM64331.html (expensive) and https://ia801403.us.archive.org/10/items/Hopcroft_Rajeev_Ullman-ItAtLnC2ed/Intro%20to%20Automata%20Theory,%20Languages%20and%20Computation,%202ed%20_%20John%20E%20Hopcroft,%20Rajeev%20Motwani,%20Jeffrey%20D%20Ullman.pdf.
• [SwA] Semantics With Applications - An Appetizer, Hanne Riis Nielson and Flemming Nielson, Springer 2007. See http://link.springer.com/book/10.1007%2F978-1-84628-692-6.
• [FM]: Formal Methods – An Appetizer, Hanne Riis Nielson and Flemming Nielson, Manuscript 2017. Will be made available on CampusNet.

 

Remarks: The course is given in English.

 

CampusNet: https://cn.inside.dtu.dk/cnnet/element/536873