Teaching Materials

  • Software Engineering using Formal Methods“ (Wolfgang Ahrendt, Richard Bubel, Chalmers University and University of Gothenburg)
    „The course introduces practically and theoretically the two most important styles of formal methods for reasoning about software: model checking and deductive verification.“
    Tools used : Spin, jSpin, SpinSpider, KeY
  • Testing, Debugging, and Verification“ (Wolfgang Ahrendt, Reiner Hähnle, Chalmers University and University of Gothenburg)
    This course teaches the principles of software verification and specification. By that it covers different methods for verifying programs.
    Tools used: JUnit, JMLUnit, KeY-Verification-Based-Test-Generation, KeY-Visual-Symbolic-Debugger, KeY-Hoare
  • Software Verification“ (Anders Møller, Aarhus University)
    This course covers various program analysis/verification tools and teaches how to apply and evaluate these tools.
    Tools used: SLAM, SPIN, CUTE, PALE and others
  • Formale Spezifikation und Verifikation“ (Prof. Bernhard Beckert, Universität Koblenz)
    This course teaches different techniques of formal verification and specification. There are additional exercises to the lecture to practice the use of KeY and other verification tools.
    Tools used: KeY, Spin
  • Formale Systeme“ (Bernhard Beckert, Universität Karlsruhe)
    This course gives an introduction to logics. It starts with Propositional and First-order logic and also covers OCL, temporal logic and automates.
    Tools used: KeY
  • Einführung in die formale Spezifikation von Software“ (Prof. Bernhard Beckert, Universität Koblenz)
    The goal of this course is for the students to become able to understand specification languages, read specifications and to create specifications on their own. JML, OCL and abstract data types are some of the topics covered in this course.
  • Formale Entwicklung objektorientierter Software“ (Prof. Peter H. Schmitt, Universität Karlsruhe)
    In this practical training a whole java based software project is developed by using JML for specification and ESC/Java2 and KeY for verification purposes.
    Tools used: ESC/Java2, KeY
  • Formale Programmentwicklung“ (Prof. Peter H. Schmitt, Universität Karlsruhe)
    A seminar about formal methods in software engineering.
  • Verification of Security Protocols“ ( Christian Haack, Radboud University Nijmegen)
    In this course the students learn techniques for black box modelling of security protocols, how to specify security requirements such as secrecy and authenticity, and learn techniques for verifying such requirements.“
  • Formal Methods“ (Dilian Gurov, Stockholm University)
    This course introduces formal methods by explaining „some important tools and techniques“.
    "During the course students will get exposed to three main approaches in the formal methods area, namely: Hoare logic and weakest precondition calculus, process algebra and process equivalences, and temporal logic model checking.“
  • „Specification and Verification of Parallel Systems“ (Einar Broch Johnsen, University of Oslo)
    "Temporal logic for the specification of invariance and liveness properties of parallel systems. Deductive techniques for proving that a parallel system satisfies a temporal logic specification. Automatic verification using model checking techniques.“
  • „Formal modelling and analysis of communicating systems“ (Einar Broch Johnsen, University of Oslo)
    This course teaches the „use of formal methods for modelling and analysing communicating distributed systems“
  • „Formal Systems and Their Applications“ (Dave Clarke, Katholieke Universiteit Leuven)
    The course is about formal methods for programming languages and type checkers. During a course project an introduction to Scala is given.
  • „Formal Programming“ (Geoff W. Hamilton, Dublin City University)
    „The module aims to enable students to use mathematical notations and techniques to enhance significantly the quality of the code they produce. They will acquire theoretical insight into the mathematics of specifying and verifying programs.“
  • „Advanced Formal Methods“ (Mads Dam, Stockholm University)
    Based on the course „Formal Methods“
    „Course contents are intended to vary from year to year.“
    Tools used: Isabelle
  • “Specification and Verification with High-Order Logic“ (Prof. Dr. Arnd Poetzsch-Heffter, Technische Universität Kaiserslautern)
    This course teaches the Fundamentals of theorem proving and covers the „High-Order Logic System“. It also covers some theorem proving applications.
    Tools used: Isabelle/HOL
  • „Beweisbar korrekte Software“ (Prof. Dr. Wolfgang Reif, Universität Augsburg)
    This course covers different techniques for specification and verification of software and specifically modular systems. The KIV – System is introduced as a tool for this purpose.
    Tools used: KIV
  • „Formal Systems“ (René Rydhof Hansen, Aalborg University)
    This course tries to provide „a deeper understanding of advanced topics within the area of Formal Systems“
  • „Software Analysis and Verification“ (Viktor Kuncak, Ecole Polytechnique Fédérale de Lausanne)
    „The topics in the class […] come from three cross-cutting themes of software analysis and verification: reasoning about programs, logic and automated reasoning, systems and methodology“
    Tools used: Jahob System, PiVC tool
  • Formal methods teaching materials from the KeY project site
  • Lecture notes on static analysis, Lecture notes on type inference, from University of Aarhus
  • Some exercises using JML and ESC/Java2, suitable for BSc students without prior exposure to formal methods
  • The Spec# Programming System  (Rosemary Monahan, NUI Maynooth) material suitable for BSc students with knowledge of Hoare Logic.