Course contents *
* 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.
Intended learning outcomes *
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.