DD2457 Programsemantik och programanalys 6,0 hp

* Part I. Operational Semantics and Language Implementation: natural semantics, structural operational semantics, abstract machines, correctness of language implementation.

* Part II. Denotational Semantics and Program Analysis: denotational semantics, fixed-point theory, program analysis and transformation.

* Part III. Axiomatic Semantics and Program Verification: axiomatic semantics, program specification and verification, weakest pre-conditions, verification condition generation.

The overall aim of the course is to study the main semantic styles used for capturing the meaning of programs in a formal way, namely operational semantics, denotational semantics and axiomatic semantics, compare their strengths and weaknesses, and use these semantics for program analysis, optimisation and verification, both in theory and as a basis for software tools.

The successful student will be able to perform constructions such as:

* Construct the state space of a program as a basis for program behaviour analysis through state space exploration.

* Translate programs to abstract machine code, and execute the latter.

* Compute the denotation of a program.

* As above, but in abstract domains.

* Extend a programming language with new language features, and extend its semantics and abstract machine implementations accordingly.

* Suggest and justify program transformations supported by a suitable program analysis.

* Specify and verify programs in Hoare logic.

* Generate verification conditions from a program with annotated while loops.

as well as be able to formally establish results such as:

* Relate different semantic styles.

* Prove language properties such as determinism and termination.

* Show correctness of a given program transformation by proving equivalence of the original and the transformed program.

* Show properties of a given semantics.

For passing the course, a student has to demonstrate proficiency with problems of the first type; for the highest grade he/she has to be equally proficient at the remaining types of problems.

För fristående kursstuderande:

DD1337 Programmering, DD1338 Algoritmer och Datastrukturer, SF1630 Diskret Matematik, DD1350 Logik för Dataloger eller motsvarande kurser.

5B1118/SF1610 Discrete Mathematics, mandatory and 5B1928/SF1642 Logic, recommended

När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.

• HEM1 - Hemuppgifter, 2,0 hp, betygsskala: P, F
• LAB1 - Laborationer, 2,0 hp, betygsskala: P, F
• TEN1 - Tentamen, 2,0 hp, betygsskala: A, B, C, D, E, FX, F

Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.

Examinator får medge annan examinationsform vid omexamination av enstaka studenter.

* LAB1 - Laboratory work, 2,0 hp, grade: Pass/fail

* HEM1 - Exercises, 2,0 hp, grade: Pass/fail

* TEN1 - Examination, 2,0 hp, grade: A, B, C, D, E, FX, F

Dilian Gurov

• Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
• Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
• Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.

Examinationen genomförs under övergångsperioden inom ramen för kursen DD2557. Kursmodulerna i DD2457 ersätts av kursmoduler i DD2557 med samma namn.