Formal Methods in Software Development (Debrecen 2015)

Section outline

• Select section General

  Collapse Expand

  General

  Collapse all Expand all

  Blocked Course, University of Debrecen, October 2015.

  http://www.risc.jku.at/people/schreine/courses/ws2015/formsd

  This course gives an overview on tools and techniques for formally specifying, checking and verifying Java programs.

  Since the exercises will be submitted via Moodle, you also have to login in Moodle and enroll as a participant of this course. You will then also receive per email all messages posted in the News forum and may yourself post messages in the Questions and Answers forum.
  

  • Select activity News forum

    

    News forum
  • Select activity Questions and Answers

    

    Questions and Answers Forum
• Select section Lecture

  Collapse Expand

  Lecture

  • Introduction
  • Formal Methods: Practice and Experience
    
  • Logic and Proving
  • The Java Modeling Language
  • Behavioral Interface Specification Languages
    
  • Extended Static Checking with ESC/Java2
  • Satisfiability Modulo Theories: Introduction and Applications
    
  • Verifying Java Programs with KeY
    

  • Select activity Java/JML Examples

    

    Java/JML Examples File
• Select section Exercises

  Collapse Expand

  Exercises

  • Select activity Assignment 1

    

    Assignment 1
  • Select activity Assignment 2

    

    Assignment 2
• Select section Software

  Collapse Expand

  Software

  The following software is used in this course (how to use the software):

  • Java Modeling Language (JML) tools
  • Use the stable release 5.5 from the archive (not the newer release candidates); also note that the JML tools need an installation of Java 1.4.2.
  • Documentation
  • OpenJML
  • Documentation
  • Extended Static Checking for Java (ESC/Java 2)
  • Documentation
  • KeY Verification Environment
  • Case Studies and Tutorials (Quicktour)