Weekly outline

  • Seminar "Formal Methods II" (SS 2013, 326.099)


    Time: Wednesday, 12:30-14:00. Place: Hagenberg Seminar Room. Start: March 6, 2013

    If you prefer another time or place (at the JKU campus), contact me per email.


    In this seminar, we explore current research and systems for specifying and verifying computer programs (specification languages, program verifiers, model checkers, ...). This continues the seminar of the previous semester.


    To take part in the seminar, you have to enrol in the KUSSS system. If you also login in Moodle and register as a course participant, you will receive per email all messages posted in the News forum.

  • 6 March - 12 March

    • Introduction and Organization
    • Wolfgang Schreiner: Performance Modeling and Analysis with the Probabilistic Model Checker PRISM.
  • 13 March - 19 March

    • Mykola Skrypskyj: Report on PhD research.
  • 20 March - 26 March

    • Rachel Sun: Report on Master Thesis
  • 17 April - 23 April

    • Taimoor Khan: Report on PhD research.
  • 24 April - 30 April

    • Alex Baumgartner: A Variant of Higher-Order Anti-Unification

    The anti-unification problem of two terms t1 and t2 is concerned with finding their generalization, a term t such that both t1 and t2 are instances of t under some substitutions. Interesting generalizations are the least general ones. The purpose of anti- unification algorithms is to compute such least general generalizations. For higher-order terms, in general, there is no unique least general higher-order generalization. Therefore, special classes have been considered for which the uniqueness is guaranteed. One of such classes is formed by higher-order patterns. These are lambda-terms where the arguments of free variables are distinct bound variables. A rule-based anti-unification algorithm in simply-typed lambda- calculus which computes a least general higher-order pattern generalization will be presented. The algorithm computes it in cubic time within linear space and it has been implemented.

  • 15 May - 21 May

    • Alexander Maletzky: The Rewriting System Maude.
  • 29 May - 4 June