Till KTH:s startsida Till KTH:s startsida

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)
  • Express language properties (such as language determinism) and program properties (such as program termination) in different semantics
  • Specify program correctness in Hoare logic (axiomatic semantics) by means of a pre-condition and a post-condition
  • Generate tests via symbolic execution (for a given coverage criterion)
  • Verify programs via symbolic execution and weakest precondition computation
Level C: Extended Concepts and Simple Proofs
  • Prove semantic equivalence of two statements:
    • in natural semantics
    • in denotational semantics
  • Extend a given semantics to new language constructs
  • Develop abstract domains for program analysis by abstract interpretation
  • Suggest and justify program transformations, supported by a suitable program analysis
Level A: Advanced Reasoning and Proofs
  • Compute denotations of statements with while loops
  • Prove language and program properties
  • Relate different semantics
  • Other theoretical problems involving proofs, 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

Dilian Gurov skapade sidan 6 mars 2017

Lärare kommenterade 18 maj 2017

Please do not neglect the material, which is not in the book, as I give equal weight to all material covered in the course. Study carefully all material in the handouts (see Course Outline), which you should print and take with you to the exam, together with the book. Do not hesitate to contact me if you need clarifications, especially if you missed some class.

Anmäl missbruk
Dilian Gurov redigerade 14 juni 2017

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)
* Express language properties (such as language determinism) and program properties (such as program termination) in different semantics
* Specify program correctness in Hoare logic (axiomatic semantics) by means of a pre-condition and a post-condition
* Generate tests via symbolic execution (for a given coverage criterion)
* Verify programs via symbolic execution and weakest precondition computation
Level C: Extended Concepts and Simple Proofs
* Prove semantic equivalence of two statements:

* in natural semantics
* in denotational semantics
* Extend a given semantics to new language constructs
* Develop abstract domains for program analysis by abstract interpretation
* Suggest and justify program transformations, supported by a suitable program analysis
Level A: Advanced Reasoning and Proofs
* Compute denotations of statements with while loops
* Prove language and program properties
* Relate different semantics
* Other theoretical problems involving proofs, 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 29 May 2017 (with partial solutions)
* 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)