Gruppwebben som samarbetsyta stängs 1 oktober 2026. Du som administratör behöver nu exportera gruppens innehåll och/eller radera gruppen.
Observera: Från och med den 1 oktober 2026 kommer delar av gruppwebben som inte längre används, successivt att stängas ned, exempelvis gruppwebbar som redan har flyttats eller varit inaktiva under en längre tid.
Mer information hittar du i nyheten: Gruppwebben och Social stänger den 1 oktober 2026. Stöd och instruktioner för hur du exporterar en gruppwebb finns i: Gruppwebben som samarbetsyta stängs 1 oktober 2026..
Course Outline
Below, you find an outline of the course with required reading and recommended exercises, both based on the course book.
Class 1 [Chapter 1.1] [slides]
- Introduction to Semantics for Programming Languages
- Course goals and syllabus
- Course organization and administration
Part I: Operational Semantics and Language Implementation
Class 2 [Chapter 1.2-1.4, 2.1] [Exercises 1.13, 2.3, 2.7]
- Syntax of the simple programming language While
- Semantics of arithmetic and Boolean expressions [Prolog]
- Definitions and proofs by structural induction
- Natural semantics (aka Big-step operational semantics) [Prolog]
- Description of Assignment 1 (see Assignments)
Class 3 [Chapter 2.2, 2.3] []
- Program termination
- Equivalence between statements [rules]
- Determinism of While
- The semantic function Sns
- Structural operational semantics (aka Small-step operational semantics)
- Configuration graphs and state space exploration [example]
Class 4 [Chapter 3] [Exercise 2.16]
- Peer assessment of Assignment 1
- The semantic function Ssos
- Equivalence of natural and structural operational semantics
- Extending While with additional language features:
- abortion
- non-determinism
- parallelism/concurrency/threads
- procedures
- Description of Assignment 2 (see Assignments)
Class 5 [Chapter 4] []
- Correct implementation of programming languages: approach
- An abstract machine: language and semantics
- A translation of While statements into abstract machine code
Class 6 [] [Exercises 4.13, 4.14, 4.19]
- Correctness as semantic equality w.r.t. specification semantics
- Description of Assignment 3 (see Assignments)
- Description of Lab Assignment 1 (see Labs)
Part II: Denotational Semantics and Program Analysis
Class 7 [Chapter 5.1] []
- Peer assessment of Assignment 2
- Peer assessment of Assignment 3
- Concluding remarks on operational semantics
- Introduction to Denotational Semantics
- The meaning of while loops
Class 8 [Chapter 5.2] [Exercises 5.18, 5.21, 5.33, 5.40]
- Fixed-point theory
Class 9 [Chapter 5.3, 5.4] [Exercises 5.49, 5.50, 5.51, 5.53]
- Summary of conditions for the Fixed Point Theorem
- Back to the denotational semantics of while loops
- Example: the denotation semantics of while ¬(x=0) do x:=x-2 [example]
- Consistency with the operational semantics of While
- Language properties expressed through denotational semantics:
- determinism
- termination
- equivalence of statements
- Description of Assignment 4 (see Assignments)
Class 10 [Chapter 7.1] []
- Introduction to Program Analysis
- Detection-of-signs analysis: Arithmetic and Boolean expressions
Class 11 [Chapter 7.4] [Exercises 7.28, 7.29] [notes]
- Detection-of-signs analysis: statements
- Detection-of-signs analysis: examples
- Application to program transformation
- Description of Assignment 5 (see Assignments)
Part III: Axiomatic Semantics and Program Verification
Class 12 [Chapter 9.2]
- Description of Lab Assignment 2 (see Labs)
- Symbolic execution [notes]
- Introduction to Axiomatic Semantics [rules]
Class 13
- Peer assessment of Assignment 4
- Peer assessment of Assignment 5
- Soundness and completeness of axiomatic semantics
- Proof tableaux: proofs as annotated programs [example-tree] [example-tableau]
- Loop invariants
- Description of Assignment 6 (see Assignments)
Class 14 [Chapter 9.3]
- Peer assessment of Assignment 6
- Automated program verification I
- symbolic execution based verification [notes]