IT-Universitetet i København
 
  Tilbage Kursusoversigt
Kursusbeskrivelse
Kursusnavn (dansk):Advanced Models and Programs 
Kursusnavn (engelsk):Advanced Models and Programs 
Semester:Forår 2014 
Udbydes under:cand.it., softwareudvikling og -teknologi (sdt) 
Omfang i ECTS:15,00 
Kursussprog:Engelsk 
Kursushjemmeside:https://learnit.itu.dk 
Min. antal deltagere:12 
Forventet antal deltagere:40 
Maks. antal deltagere:70 
Formelle forudsætninger:Generally:

  • Solid knowledge of the Java and C# programming languages. (Knowledge of at least one more programming language, particulary a functional language like ML, Haskell, or Lisp, is helpful).

  • Basic knowledge of mathematical foundations of programming and program reasoning (i.e., the idea that we'll talk about sets, sequences, types, etc. does not scare you off).

  • Basic knowledge of model-driven development and the underlying idea of models, relating model to models, and relating models to code. For example, understanding the basics of UML or a similar modeling language, understanding how mathematical models like sequences and sets are used to specify algorithms, or understanding how an AST is an algebraic model for a programming language, is adequate background knowledge.


Knowledge of programming languages and foundations of computing as represented in the following courses:

  • Programming Languages Concepts and Implementation (SPLC)

  • Foundations of Computing: Discrete Mathematics (SGDM)

  • Foundations of Computing: Algorithms and Data Structures (SGDS)


These courses can be taken in parallel, though preferably they will have been completed prior to taking this course.

Additionally, material covered in the following courses complement that which this course covers, so taking them prior to this course helps, but taking them in parallel or after is permitted.

  • Model Driven Development (KF30)

  • Object Oriented Programming (OOP)

  • System Architecture and Security (SSAS)

 
Læringsmål:The course has two major parts as detailed under course form below---a regular course followed by a project.

After the course, the students are expected to be able to:

  • describe relevant concepts within the themes of the course,

  • account for the practical applications of the covered constructs, and

  • compare selected techniques and constructions within a single of the course themes.


On the basis of the project, the students are expected to be able to:

  • apply relevant methods and techniques in the chosen project,

  • argue for the overall design-decisions in, and correctness properties of, the project, and

  • relate the project to the underlying theory.

 
Fagligt indhold:The subject of the course is programming language foundations and technologies, with special attention to advanced technologies that are likely to influence software practice over the next ten years.

The contents of the course is structured in three themes.

1. Axiomatic Reasoning about Models and Programs

In particular, their pragmatic use in program design via model-driven development, implementation, validation, and verification.

The material and structure for this part of the course will come from Benjamin Pierce's Software Foundations course using the Coq proof assistant.

http://www.cis.upenn.edu/~bcpierce/sf/

https://coq.inria.fr/

2. Verifying imperative programs

We will cover operational and axiomatic semantics of imperative programming languages. We will use Hoare Logic and Separation Logic to write specifications for and prove the correctness of imperative programs.

We will verify Java Programs using the Coq proof assistant and Kopitiam.
Kopitiam is an Eclipse plugin that integrates the standard Java development environment with Coq, allowing programs and their proofs of correctness to be developed in one framework.

https://itu.dk/research/tomeso/kopitiam/

3. Rigorous Software Engineering and Testing

In particular, the concepts, tools, and techniques used for analysis and design of programs, one example being QuickCheck for Java.

http://quickcheck.java.net/ 
Læringsaktiviteter:14 ugers undervisning bestående af forelæsninger, øvelser og vejledning

The course period is 16 weeks half time (15 ects). The course consists of:


  • Lectures and exercises (approximately 10 weeks), covering the themes of the course.

  • A project done in groups of 1-3 students (approximately 6 weeks), within one of the themes, resulting in a project report.


The weekly exercises must be handed in, and all of the exercises must be approved to pass the course. The project report must be presented in an oral exam, where questions may be asked in all themes of the course.

Projects are of any sort so long as they relate to the course materials and have both a theoretical and an engineering component. 
Obligatoriske aktivititer:All assignments listed here may be done in groups of 1-3 students.


  • There will be eight weekly hand-in assignments, all of which you must pass before you start your projects. An exact date will be given at the start of the course.

  • There will be one mandatory presentation of software verification tools used in industry and/or academia. An exact date will be given at the start of the course.

  • A project spanning approximately six weeks must be handed in. An exact handing date will be given at the start of the course.
 
Eksamensform og -beskrivelse:X. experimental examination form (7-scale; external exam), 7-trins-skala, Ekstern censur

The weekly exercises must be handed in, and all exercises must be approved to pass the course. The project report must be presented in an oral exam, where questions may be asked in all themes of the course.

The duration of this oral exam is 30 minutes.  

Litteratur udover forskningsartikler:To be announced. 
 
Afholdelse (tid og sted)
Kurset afholdes på følgende tid og sted:
UgedagTidspunktForelæsning/ØvelserStedLokale
Mandag 10.00-11.50 Forelæsning ITU 2A20
Mandag 12.00-13.50 Øvelser ITU 2A20, 4A56
Onsdag 12.00-13.50 Øvelser ITU 2A20, 4A56
Onsdag 14.00-15.50 Forelæsning ITU 2A20

Eksamen afholdes på følgende tid og sted:
EksamensdatoTidspunktEksamenstypeStedLokale
2014-05-21 14:00 Skriftlige arbejder ITU To be uploaded in learnIT
2014-06-20 08:00-18:00 Mundtlig eksamen ITU 4A20
2014-08-15 13:00-14:00 re-eksamen Mundtlig eksamen ITU 2A18