• OGO 2.2 Softwarespecificatie (2IO35), week 6-14, 2011-2012.

  • Algorithms for Model Checking,  2007-2014.
    Treats the mu-calculus and CTL* and its subsets LTL and CTL, and various approaches and algorithms for verifying formulae in these logics. These include the standard labelling algorithms and the symbolic (fixed point based) algorithms for CTL, and fair CTL. The Emerson-Lei algorithm for verifying the mu-calculus is analysed and discussed. Transformations of the model checking problem to the frameworks of Boolean equation systems and Parity Games are addressed, combined with advanced algorithms for solving the latter artefacts. See the 2014, 2013, 2012, 2011, 2010, 2009, 2008 and 2007 editions
  • Software Specification,  2008-2011.
    Discusses the various stages of a software product, and the artefacts involved. Uses UML use cases, class diagrams, sequence diagrams and state charts to describe these artefacts, and addresses the use of Z and temporal logic. Discusses the consistency requirements and the relations between all artefacts.