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, among others, to (with approximate levels):

Level E: Basic Constructions
* 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 verificationGenerate tests via symbolic execution (for a program annotated withgiven coverage criterion)
* Verify programs via symbolic execution and weakest pre-condition, post-condition and loop invariants)
Level C computation
Level C: Extended Concepts and Simple Proofs
* Provinge 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: Advanced Reasoning and Proofs
* Computinge denotations of while loops:

* in the concrete domain (and interpreting the approximants)
* in abstract domainstatements with while loops
* Provinge language and program properties
* Verifying programs in Hoare logic, tableau-style:

* finding loop invariants
* completing the annotation
* identifying and justifying the proof obligations
* RelatingRelate different semantics
* Other theoretical problems involving proofs, such as:

*including 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)