Till KTH:s startsida Till KTH:s startsida

Course Literature

Book cover

Nielson and Nielson
Semantics with Applications: An Appetizer
Springer-Verlag, 2007, ISBN: 978-1-84628-691-9
Available from Kårbokhandeln at the start of the period, and electronically from the KTH library.

In addition: some hand-written slides on axiomatic semantics and verification condition generation (see outline, part III), and a text explaining the principle of structural induction.

Here are my own LaTeX definitions. Derivation trees I create with the following package.

Additional reading for the curious student:

  • A paper from 2003 formalizing the Java Virtual Machine and Language, and thus providing an abstract machine semantics for the Java bytecode language JVML.
  • A paper from 2009 comparing various operational semantics by means of rewriting logic.
  • A paper from 2016 on provably correct extraction of program models from Java bytecode, related to the topic of provably correct implementation of programming languages.
  • The original paper by J. King from 1976 on symbolic execution and testing.
  • The original paper by C.A.R. Hoare from 1969 on axiomatic semantics.
  • The original paper by Bertrand Meyer from 1992 on design-by-contract as a Hoare logic based approach to software development.
  • A paper comparing (forward) symbolic execution against (backward) weakest precondition calculation for Hoare logic based program verification.

Dilian Gurov skapade sidan 6 mars 2017

Dilian Gurov redigerade 21 mars 2017

Book cover

Nielson and Nielson Semantics with Applications: An Appetizer Springer-Verlag, 2007, ISBN: 978-1-84628-691-9 Available from Kårbokhandeln at the start of the period. In addition: some hand-written slides on axiomatic semantics and verification condition generation (see outline, part III), and a text explaining the principle of structural induction.

Here are my own LaTeX definitions. Derivation trees I create with the following package. Additional reading for the curious student:


* a paper by Freund and Mitchell formalizing the Java Virtual Machine and Language, thus providing an abstract machine semantics for the Java bytecode language JVML.