Seminar Formal Methods I (WS 2019/20)

Section outline

• Select section Seminar Formal Methods I (WS 2019/20)

  Seminar Formal Methods I (WS 2019/20)

  Collapse all Expand all

  326.063, Thursday 13:45-15:15, JKU Campus, Start: October 10

  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 Announcements

    

    Announcements Forum
• Select section October 9 (MZ 005A)

  October 9 (MZ 005A)

  • Wolfgang Schreiner: Introduction and Organization
    
• Select section October 31 (S3 048)

  October 31 (S3 048)

  • Lucas Payr: presentation of master thesis
  • Franz Reichl: presentation of master thesis
    

  • Select activity Refinement Types for Elm

    

    Refinement Types for Elm File
  • Select activity The Integration of SMT Solvers into the RISCAL Model Checker

    

    The Integration of SMT Solvers into the RISCAL Model Checker File
• Select section November 14 (MZ 003A)

  November 14 (MZ 003A)

  • Johannes Grünberger: presentation of bachelor thesis
    

  • Select activity Specification and Verification of Algorithms from Computational Logic

    

    Specification and Verification of Algorithms from Computational Logic File
• Select section November 28 (K 012D)

  November 28 (K 012D)

  • Michael Wipplinger: ACSL & Frama-C

  • Select activity Frama-C and ACSL

    

    Frama-C and ACSL File
• Select section January 31 (14:30-16:00, S2 054)

  January 31 (14:30-16:00, S2 054)

  • Michael Wipllinger: ACSL & Frama-C (2nd talk)
  • Lucas Payr: 2nd presentation of master thesis
  • Franz Reichl: 2nd presentation of master thesis
  
  

  • Select activity The Integration of SMT Solvers into the RISCAL Model Checker

    

    The Integration of SMT Solvers into the RISCAL Model Checker File
  • Select activity Refinement Types for Elm

    

    Refinement Types for Elm File
  • Select activity Automated Proving in Frama-C

    

    Automated Proving in Frama-C File