- „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.
|
|
