Examination

The requirement for the course is a pass on the assignments, the lab assignments, and the written exam. The grade will be the grade obtained at the written exam. You're allowed to bring the course book, hand-outs and own lecture notes taken in class.

Note that you must be registered for the course in order to have the result of your exam reported.

Grading

The exam will be graded based on the intended learning outcomes of the course, classified in three levels. After the course, students will be able to (with approximate levels):

Level E

• Execute statements in:
• natural semantics, i.e. derive transitions
• structural operational semantics, i.e. construct the configuration space and draw the configuration graph
• abstract machine semantics, i.e. translate statements to abstract machine code and execute the code
• denotational semantics, i.e. compute denotations (for loop-free programs)
• Expressing language properties (such as language determinism) and program properties (such as program termination) in different semantics
• Specifying program correctness in Hoare logic (axiomatic semantics) by means of a pre-condition and a post-condition
• Program verification via symbolic execution (for a program annotated with pre-condition, post-condition and loop invariants)

Level C

• Proving semantic equivalence of two statements:
• in natural semantics
• in denotational semantics
• Extending a given semantics to new language constructs
• Developing abstract domains for program analysis by abstract interpretation
• Computing and interpreting abstract denotations for loop-free programs
• Suggesting and justifying program transformations, supported by a suitable program analysis

Level A

• Computing denotations of while loops:
• in the concrete domain (and interpreting the approximants)
• in abstract domains
• Proving language and program properties
• Verifying programs in Hoare logic, tableau-style:
• finding loop invariants
• completing the annotation
• identifying and justifying the proof obligations
• Relating different semantics
• Other theoretical problems involving proofs, such as:
• problems from fixed-point theory

Bonus points will be taken into account, namely one bonus point per homework assignment handed in on time.

Exam resits

Exam resits (sv. omtentor) are by mutual arrangement with the lecturer.

Previous Exams

• exam from 3 June 2015 (with partial solutions)
• exam from 21 May 2013 (with partial solutions)
• exam from 26 May 2011 (with hand-written solutions)
• exam from 14 December 2009 (with solutions)