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)

Any news on whether the digital course book will be allowed on the exam? If it is not allowed, are you allowed to bring printed pages from the book?

Also, are the only allowed notes those taken during lectures, or can you bring any of your own notes?

Cheers.

See my latest post regarding th book. What exactly do you mean by "own notes not taken in class"? I definitely don't want that you bring own notes of previous exams. :-)

Yeah, I understand that concern. Basically when I study for exams I typically take notes on things I have trouble with, which may or may not come from a previous exam. I guess it's a matter of definition, but I'll avoid bringing other notes to be sure.