Seminar Formal Methods I (WS 2017/18)

Section outline

• Select section General

  General

  Collapse all Expand all

  326.063, Wednesday, 12:30-13:00, Seminar Room Castle Hagenberg, Start: October 18
  

  If you prefer another time or place (e.g., at the JKU campus), send me an 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 Announcements

    

    Announcements Forum
• Select section 4 December - 10 December

  4 December - 10 December

  • Monday, December 4, 16:15-17:45, S3 057
    
  • Binder: PRISM  (stochastic model checking)
  • Plank: PRISM (probabilistic model checking)
    
  • Thursday,December 7, 16:15-17:45, S3 048
    
  • Reichl: Facebook Infer & Separation Logic

  Preparatory meetings: Friday, November 24, 13:45, S2 0327 (individual times to be announced)
  

  • Select activity Binder: Prism and CMTC

    

    Binder: Prism and CMTC File
  • Select activity Plank: Prism for Discrete Time Markov Chains

    

    Plank: Prism for Discrete Time Markov Chains File
  • Select activity Reichl: Facebook Infer

    

    Reichl: Facebook Infer File
  • Select activity Examples

    

    Examples File
• Select section 29 January - 4 February

  29 January - 4 February

  • Monday, January 29, 16:30-18:00, S2 054
    
  • Binder: PRISM  (stochastic model checking)
  • Plank: PRISM (probabilistic model checking)
    
  • Thursday, February 1, 16:30-18:00, S3 047
    
  • Reichl: Facebook Infer & Separation Logic

  Preparatory meetings: Friday, January 19, 13:45, S2 0327 (individual times to be announced)
  

  • Select activity Plank: PRISM for Discrete Time Markov Chains

    

    Plank: PRISM for Discrete Time Markov Chains File
  • Select activity Binder: PRISM and CTMC

    

    Binder: PRISM and CTMC File
  • Select activity Reichl: Separation Logic and Bi-Abduction

    

    Reichl: Separation Logic and Bi-Abduction File