Seminar "Formal Methods II" (SS 2013)

Section outline

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

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

  Collapse all Expand all

  ---

  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.

  • Select activity News forum

    

    News forum
  • Select activity Questions and Answers

    

    Questions and Answers Forum
• Select section 6 March - 12 March

  6 March - 12 March

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

  13 March - 19 March

  • Mykola Skrypskyj: Report on PhD research.

  • Select activity Cloud Computing to Simulate the Movement of Pollutants in the Atmosphere

    

    Cloud Computing to Simulate the Movement of Pollutants in the Atmosphere File
• Select section 20 March - 26 March

  20 March - 26 March

  • Rachel Sun: Report on Master Thesis

  • Select activity A Language for Building Web Interfaces to Mathematical Software

    

    A Language for Building Web Interfaces to Mathematical Software File
• Select section 17 April - 23 April

  17 April - 23 April

  • Taimoor Khan: Report on PhD research.

  • Select activity Formal Verication of MiniMaple Programs

    

    Formal Verication of MiniMaple Programs File
• Select section 24 April - 30 April

  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.

  • Select activity A Variant of Higher-Order Anti-Unication

    

    A Variant of Higher-Order Anti-Unication File
• Select section 15 May - 21 May

  15 May - 21 May

  • Alexander Maletzky: The Rewriting System Maude.

  • Select activity Introduction to Maude

    

    Introduction to Maude File
• Select section 29 May - 4 June

  29 May - 4 June

  • Wolfgang Schreiner: The TLA Toolbox