Formal Methods Courses around the World

Courses on Actress

Course : Action Semantics and Compiler Generation [Ref: ascg-01]

• Year :
• Offered at: Aarhus
• Contact :P.D. Mosses
• Topics : Action Semantics
• Languages :
• Tools : RAT ; RML ; Actress

Courses on Alloy

Course : Software Engineering Environments [Ref: 475]

• Year :
• Offered at: Imperial C.
• Contact :M. Huth
• Topics : Formal program techniques
• Languages : Alloy
• Tools : Alloy

Course : Software Engineering -- Methods [Ref: 302]

• Year :
• Offered at: Imperial C.
• Contact :M. Huth
• Topics : Formal program techniques
• Languages : Alloy
• Tools : Alloy

Course : Software Engineering II [Ref : Without a reference name]

• Year :
• Offered at: Milan Poli.
• Contact :C. Ghezzi
• Topics : Model Checking ; Software Testing
• Languages :
• Tools : SPIN ; Alloy

Course : Formal Methods Laboratory [Ref: LAB-MF]

• Year : 5
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics :
• Languages : B-Method ; VDM++ ; Alloy
• Tools : VDMTools

Courses on AtelierB^?

Course : Specification and Formal Verification in B [Ref : Without a reference name]

• Year : 5/ MSc
• Offered at: Bordeaux
• Contact :G.Sutre
• Topics : Program verification ; Algorithm refinement
• Languages : B-Method
• Tools : B-Toolkit ; Atelier-B

Course : Model-Oriented Formal Methods [Ref: MSF-CA]

• Year : MSc
• Offered at: Nantes
• Contact :J.C. AttiogbÈ
• Topics :
• Languages : B-Method ; Z-Notation
• Tools : ZTC ; ZANS ; Z/EVES ; Atelier-B

Courses on B

Course : Formal Methods [Ref : Without a reference name]

• Year : MSc
• Offered at: Beira-Interior
• Contact :S.M. Sousa
• Topics : Hoare Logic ; DMat
• Languages : B-Method ; The CAML Language
• Tools : COQ ; WHY

Course : Specification and Formal Verification in B [Ref : Without a reference name]

• Year : 5/ MSc
• Offered at: Bordeaux
• Contact :G.Sutre
• Topics : Program verification ; Algorithm refinement
• Languages : B-Method
• Tools : B-Toolkit ; Atelier-B

Course : Program Verification and Specification [Ref: CS03PV]

• Year : 3
• Offered at: London (K.C.)
• Contact :D. Clark
• Topics : Model Checking ; Program verification
• Languages : B-Method
• Tools :

Course : Techniques de preuve et vÈrification formelle [Ref : Without a reference name]

• Year : MSc
• Offered at: Marseille
• Contact :J.-R. Abrial
• Topics : Model Checking ; Abstract State Machines
• Languages : B-Method
• Tools :

Course : MÈthodes Formelles [Ref : Without a reference name]

• Year : MSc
• Offered at: Metz
• Contact :D. Cansell
• Topics : Formal program techniques
• Languages : B-Method
• Tools :

Course : Formal methods for concurrent and distributed systems [Ref : Without a reference name]

• Year : 4
• Offered at: Milan Poli.
• Contact :D. Mandrioli
• Topics : Hoare Logic ; Temporal Logic ; Refinement in B ; Petri Nets
• Languages : B-Method
• Tools : TRIO

Course : Formal Methods Laboratory [Ref: LAB-MF]

• Year : 5
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics :
• Languages : B-Method ; VDM++ ; Alloy
• Tools : VDMTools

Course : Inform. Syst. Specification and Modelling [Ref : Without a reference name]

• Year : 5/ MSc
• Offered at: Nancy
• Contact :D. MÈry
• Topics : DMat
• Languages : B-Method
• Tools :

Course : Formal Methods Integration [Ref: IFM-CA]

• Year : MSc 1-2
• Offered at: Nantes
• Contact :J.C. AttiogbÈ
• Topics : Process Algebras ; Multi-paradigm Specifications
• Languages : B-Method ; CCS ; CSP
• Tools :

Course : Model-Oriented Formal Methods [Ref: MSF-CA]

• Year : MSc
• Offered at: Nantes
• Contact :J.C. AttiogbÈ
• Topics :
• Languages : B-Method ; Z-Notation
• Tools : ZTC ; ZANS ; Z/EVES ; Atelier-B

Course : MÈthode de spÈcification formelle B [Ref:       ]

• Year :
• Offered at: Nantes
• Contact :H. Habrias
• Topics :
• Languages : B-Method
• Tools :

Course : Machine-Assisted Software Engineering [Ref: MAS]

• Year : M
• Offered at: Oxford
• Contact :J. Davies
• Topics :
• Languages : B-Method
• Tools : B-Toolkit

Course : MÈthodes Formelles de spÈcification des SystËmes Informatiques [Ref: MF]

• Year : 5
• Offered at: Paris (ENST)
• Contact :S. Vignes
• Topics :
• Languages : B-Method ; Z-Notation
• Tools :

Course : SpÈcifications Formelles [Ref : Without a reference name]

• Year : 4/5
• Offered at: Poitiers
• Contact :E. Andres (contact)
• Topics : Formal Semantics ; Formal program techniques
• Languages : B-Method
• Tools :

Course : Critical Systems [Ref: CM314]

• Year : 3
• Offered at: Southampton
• Contact :M.J. Butler
• Topics : Refinement in B ; Safety Analysis Techniques
• Languages : B-Method
• Tools : B-Toolkit

Courses on BDDC

Course : Logics and Verification [Ref : Without a reference name]

• Year :
• Offered at: Paris VII
• Contact :P. Habermehl
• Topics : Model Checking ; Temporal Logic ; BDD
• Languages :
• Tools : BBDC

Courses on Btlk

Course : Specification and Formal Verification in B [Ref : Without a reference name]

• Year : 5/ MSc
• Offered at: Bordeaux
• Contact :G.Sutre
• Topics : Program verification ; Algorithm refinement
• Languages : B-Method
• Tools : B-Toolkit ; Atelier-B

Course : Machine-Assisted Software Engineering [Ref: MAS]

• Year : M
• Offered at: Oxford
• Contact :J. Davies
• Topics :
• Languages : B-Method
• Tools : B-Toolkit

Course : Critical Systems [Ref: CM314]

• Year : 3
• Offered at: Southampton
• Contact :M.J. Butler
• Topics : Refinement in B ; Safety Analysis Techniques
• Languages : B-Method
• Tools : B-Toolkit

Courses on CADiZ^?

Course : Software and Systems Design [Ref: CO508]

• Year : BSc 2
• Offered at: Kent
• Contact :R. Lemos
• Topics :
• Languages : Z-Notation
• Tools : CADiZ

Courses on CADP

Course : Formal Methods [Ref: CO861]

• Year : MSc
• Offered at: Kent
• Contact :H. Bowman
• Topics : Model Checking
• Languages : Object-Z ; LOTOS
• Tools : CADP

Courses on CASL

Course : Techniques of Correct Software Development [Ref: TEKS]

• Year :
• Offered at: Bremen
• Contact :C. L¸th
• Topics : Model Checking ; ADT
• Languages : CSP ; CASL
• Tools : FDR ; Isabelle

Course : Algebraic Specification [Ref : Without a reference name]

• Year :
• Offered at: Bremen
• Contact :L. Schrˆder
• Topics : ADT
• Languages : CASL
• Tools :

Course : Foundations of Systems Development [Ref : Without a reference name]

• Year :
• Offered at: L-M-U M¸nchen
• Contact :M. Wirsing
• Topics : Model Checking ; ADT ; Formal program techniques ; LTL ; TLA
• Languages : Z-Notation
• Tools : CASL ; SPIN

Course : Formal Specification of Data and Process Types [Ref: FSDPT]

• Year :
• Offered at: T.U. Dresden
• Contact :Horst Reichel
• Topics : Process Algebras ; ADT
• Languages : CASL
• Tools :

Courses on CCS

Course : Semantics and Verification 2002 [Ref: F01-Dat4]

• Year :
• Offered at: Aalborg
• Contact :A. IngÛlfsdÛttir
• Topics : Process Algebras ; BDD
• Languages : CCS
• Tools : CWB ; UPPAAL

Course : Systems, Automata, and Coalgebras [Ref : Without a reference name]

• Year :
• Offered at: Bremen
• Contact :L. Schrˆder
• Topics : Process Algebras
• Languages : CCS
• Tools :

Course : Programming Method. IV (Concurrency) [Ref: MP-IV]

• Year : 3
• Offered at: Minho
• Contact :L.S. Barbosa
• Topics : Process Algebras ; Pi-Calculus
• Languages : CCS
• Tools : CWB ; PICT

Course : Formal Methods Integration [Ref: IFM-CA]

• Year : MSc 1-2
• Offered at: Nantes
• Contact :J.C. AttiogbÈ
• Topics : Process Algebras ; Multi-paradigm Specifications
• Languages : B-Method ; CCS ; CSP
• Tools :

Courses on CommUnity^?

Course : Advanced System Design [Ref: CO7205]

• Year :
• Offered at: Leicester
• Contact :J. Fiadeiro
• Topics : Software architecture
• Languages : Unity
• Tools : CommUnity

Courses on Coq

Course : Formal Methods [Ref : Without a reference name]

• Year : MSc
• Offered at: Beira-Interior
• Contact :S.M. Sousa
• Topics : Hoare Logic ; DMat
• Languages : B-Method ; The CAML Language
• Tools : COQ ; WHY

Course : Theory of Computation [Ref : Without a reference name]

• Year : 3
• Offered at: Beira-Interior
• Contact :S.M. Sousa
• Topics : Functional Programming ; DMat ; Lambda Calculus
• Languages : The CAML Language
• Tools : COQ

Course : Programmation fonctionnelle et preuves [Ref : Without a reference name]

• Year :
• Offered at: Lyon
• Contact :Y. Bertot
• Topics : Functional Programming ; TT ; Lambda Calculus
• Languages : The CAML Language
• Tools : COQ

Course : SpÈcifications formelles, connaissances et raisonnement [Ref : Without a reference name]

• Year : MSc
• Offered at: Strasbourg
• Contact :P. Gancarski (contact)
• Topics : Program verification ; Lambda Calculus
• Languages :
• Tools : COQ

Courses on CSP

Course : Techniques of Correct Software Development [Ref: TEKS]

• Year :
• Offered at: Bremen
• Contact :C. L¸th
• Topics : Model Checking ; ADT
• Languages : CSP ; CASL
• Tools : FDR ; Isabelle

Course : Systems and Software Engineering [Ref: CS L3]

• Year : S2
• Offered at: London (S.B.)
• Contact :A. Abdallah
• Topics :
• Languages : Z-Notation ; CSP ; Haskell
• Tools :

Course : Formal Methods Integration [Ref: IFM-CA]

• Year : MSc 1-2
• Offered at: Nantes
• Contact :J.C. AttiogbÈ
• Topics : Process Algebras ; Multi-paradigm Specifications
• Languages : B-Method ; CCS ; CSP
• Tools :

Course : Specification of Reactive Systems [Ref : Without a reference name]

• Year :
• Offered at: Oldenburg
• Contact :H. Wehrheim
• Topics :
• Languages : CSP
• Tools : FDR ; SPIN

Course : Advanced Concurrency Tools [Ref: ACT]

• Year : M
• Offered at: Oxford
• Contact :J. Davies
• Topics :
• Languages : CSP
• Tools : FDR

Course : Concurrency and Distributed Systems [Ref: CDS]

• Year : M
• Offered at: Oxford
• Contact :J. Davies
• Topics :
• Languages : CSP
• Tools : FDR

Course : System Analysis - Análisis de Sistemas [Ref: AS]

• Year :
• Offered at: Rosario
• Contact :M. Cristiá
• Topics : Formal Modeling^?
• Languages : CSP^? ; Z^? ; TLA^? ; Statecharts^?
• Tools : Z/EVES

Courses on CWB

Course : Semantics and Verification 2002 [Ref: F01-Dat4]

• Year :
• Offered at: Aalborg
• Contact :A. IngÛlfsdÛttir
• Topics : Process Algebras ; BDD
• Languages : CCS
• Tools : CWB ; UPPAAL

Course : Programming Method. IV (Concurrency) [Ref: MP-IV]

• Year : 3
• Offered at: Minho
• Contact :L.S. Barbosa
• Topics : Process Algebras ; Pi-Calculus
• Languages : CCS
• Tools : CWB ; PICT

Courses on ELotos

Course : Distributed Systems [Ref: CO610]

• Year : BSc 3
• Offered at: Kent
• Contact :E.A. Boiten
• Topics :
• Languages : SDL ; E-LOTOS ; Estelle
• Tools :

Courses on ESCJava

Course : Formal Methods in the Software Life Cycle [Ref: OOTI]

• Year :
• Offered at: Eindhoven
• Contact :E. Vink
• Topics : Model Checking ; Program verification
• Languages : JML
• Tools : ESC/Java 2

Courses on Estelle

Course : Distributed Systems [Ref: CO610]

• Year : BSc 3
• Offered at: Kent
• Contact :E.A. Boiten
• Topics :
• Languages : SDL ; E-LOTOS ; Estelle
• Tools :

Courses on FDR

Course : Techniques of Correct Software Development [Ref: TEKS]

• Year :
• Offered at: Bremen
• Contact :C. L¸th
• Topics : Model Checking ; ADT
• Languages : CSP ; CASL
• Tools : FDR ; Isabelle

Course : Specification of Reactive Systems [Ref : Without a reference name]

• Year :
• Offered at: Oldenburg
• Contact :H. Wehrheim
• Topics :
• Languages : CSP
• Tools : FDR ; SPIN

Course : Advanced Concurrency Tools [Ref: ACT]

• Year : M
• Offered at: Oxford
• Contact :J. Davies
• Topics :
• Languages : CSP
• Tools : FDR

Course : Concurrency and Distributed Systems [Ref: CDS]

• Year : M
• Offered at: Oxford
• Contact :J. Davies
• Topics :
• Languages : CSP
• Tools : FDR

Courses on FSP

Course : Formal Methods for Software Engineering [Ref: 213520]

• Year :
• Offered at: Twente
• Contact :E. Brinksma
• Topics : Process Algebras
• Languages : Z-Notation ; FSP ; SDL
• Tools : LTSA ; Z/EVES

Courses on FuZZ^?

Course : Specification and Design [Ref: SDE]

• Year : M
• Offered at: Oxford
• Contact :A. Martin
• Topics :
• Languages : Z-Notation
• Tools : FuZZ

Courses on GHC

Course : Programming Methodology I [Ref: MP-I]

• Year : 2
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics : Functional Programming ; Algebra of Programming
• Languages : Haskell
• Tools : GHC ; Hugs

Courses on Gofer

Course : Functional Programming [Ref: FPR]

• Year : M
• Offered at: Oxford
• Contact :J. Gibbons
• Topics : Functional Programming
• Languages : Haskell
• Tools : Hugs ; Gofer

Courses on Haskell

Course : Specification and synthesis of Haskell programs [Ref: SS03]

• Year :
• Offered at: Bremen
• Contact :T. Mossakowski
• Topics : Functional Programming ; Algebra of Programming
• Languages : Haskell
• Tools :

Course : System Modelling and Specification [Ref: 4ICT8]

• Year :
• Offered at: Dublin
• Contact :A. Hughes
• Topics : Mathematics of Program Construction
• Languages : Irish VDM ; Haskell
• Tools : IVDM Library

Course : Systems and Software Engineering [Ref: CS L3]

• Year : S2
• Offered at: London (S.B.)
• Contact :A. Abdallah
• Topics :
• Languages : Z-Notation ; CSP ; Haskell
• Tools :

Course : Programming Methodology I [Ref: MP-I]

• Year : 2
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics : Functional Programming ; Algebra of Programming
• Languages : Haskell
• Tools : GHC ; Hugs

Course : Functional Programming [Ref: FPR]

• Year : M
• Offered at: Oxford
• Contact :J. Gibbons
• Topics : Functional Programming
• Languages : Haskell
• Tools : Hugs ; Gofer

Course : Theory of Computation [Ref: TC]

• Year : 4
• Offered at: Porto
• Contact :M. Florido
• Topics : Formal Semantics ; TT ; DMat ; Lambda Calculus
• Languages : Prolog ; Haskell
• Tools :

Course : Functional programming in Standard ML [Ref : Without a reference name]

• Year : 3/4
• Offered at: Warsaw
• Contact :A. Tarlecki
• Topics : Functional Programming ; Formal Semantics ; FOL ; Formal program techniques ; Lambda Calculus
• Languages : Standard ML ; Haskell
• Tools :

Courses on HOL

Course : Specification and Verification [Ref : Without a reference name]

• Year :
• Offered at: T.U. M¸nchen
• Contact :T. Nipkow
• Topics : Automated theorem proving ; FOL ; Formal program techniques
• Languages : Standard ML
• Tools : HOL ; Isabelle

Courses on Hugs

Course : Programming Methodology I [Ref: MP-I]

• Year : 2
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics : Functional Programming ; Algebra of Programming
• Languages : Haskell
• Tools : GHC ; Hugs

Course : Functional Programming [Ref: FPR]

• Year : M
• Offered at: Oxford
• Contact :J. Gibbons
• Topics : Functional Programming
• Languages : Haskell
• Tools : Hugs ; Gofer

Courses on INA

Course : Programming Logics III [Ref: ELP-III]

• Year : 3
• Offered at: Minho
• Contact :J.M. ValenÁa
• Topics : Model Checking ; Petri Nets
• Languages :
• Tools : Integrated Net Analyzer ; Programming Enviroment based on Petri Nets ; NuSMV

Courses on Isabelle

Course : Techniques of Correct Software Development [Ref: TEKS]

• Year :
• Offered at: Bremen
• Contact :C. L¸th
• Topics : Model Checking ; ADT
• Languages : CSP ; CASL
• Tools : FDR ; Isabelle

Course : Specification and Verification [Ref : Without a reference name]

• Year :
• Offered at: T.U. M¸nchen
• Contact :T. Nipkow
• Topics : Automated theorem proving ; FOL ; Formal program techniques
• Languages : Standard ML
• Tools : HOL ; Isabelle

Course : Programming Language Semantics [Ref : Without a reference name]

• Year :
• Offered at: T.U. M¸nchen
• Contact :T. Nipkow
• Topics : Formal Semantics ; Hoare Logic ; TT ; Automated theorem proving
• Languages :
• Tools : Isabelle

Courses on IVDM

Course : System Modelling and Specification [Ref: 4ICT8]

• Year :
• Offered at: Dublin
• Contact :A. Hughes
• Topics : Mathematics of Program Construction
• Languages : Irish VDM ; Haskell
• Tools : IVDM Library

Course : Information Systems (part II) [Ref: 4BA1]

• Year :
• Offered at: Dublin
• Contact :M. Airchinnigh
• Topics : Formal Semantics ; Mathematics of Program Construction
• Languages : Irish VDM
• Tools :

Courses on IVDMH

Course : System Modelling and Specification [Ref: 4ICT8]

• Year :
• Offered at: Dublin
• Contact :A. Hughes
• Topics : Mathematics of Program Construction
• Languages : Irish VDM ; Haskell
• Tools : IVDM Library

Courses on JML

Course : Formal Methods in the Software Life Cycle [Ref: OOTI]

• Year :
• Offered at: Eindhoven
• Contact :E. Vink
• Topics : Model Checking ; Program verification
• Languages : JML
• Tools : ESC/Java 2

Reference : QS

• Year : 3
• Offered at: TU Graz
• Contact : Bernhard Aichernig
• Topics : Design by Contract ; Software Testing
• Languages : JML
• Tools : JML Tools

Courses on LOTOS

Course : Formal Methods [Ref: CO861]

• Year : MSc
• Offered at: Kent
• Contact :H. Bowman
• Topics : Model Checking
• Languages : Object-Z ; LOTOS
• Tools : CADP

Course : Software Engineering [Ref : Without a reference name]

• Year : 4
• Offered at: Lisbon
• Contact :R.G. Crespo
• Topics :
• Languages : Z-Notation ; LOTOS
• Tools :

Courses on Lotrec

Course : Methodes formelles, verification, model checking [Ref: FORMEL]

• Year : S7
• Offered at: Brest
• Contact :L. MarcÈ
• Topics : Model Checking ; CTL ; LTL
• Languages :
• Tools : LOTREC

Courses on LTSA

Course : Formal Methods for Software Engineering [Ref: 213520]

• Year :
• Offered at: Twente
• Contact :E. Brinksma
• Topics : Process Algebras
• Languages : Z-Notation ; FSP ; SDL
• Tools : LTSA ; Z/EVES

Courses on MSC

Course : Testing and Verification [Ref: TOV04]

• Year :
• Offered at: Aalborg
• Contact :K.G. Larsen
• Topics : Model Checking ; Program verification ; Software Testing
• Languages : MSC
• Tools : UPPAAL

Courses on NuSMV^?

Course : Programming Logics III [Ref: ELP-III]

• Year : 3
• Offered at: Minho
• Contact :J.M. ValenÁa
• Topics : Model Checking ; Petri Nets
• Languages :
• Tools : Integrated Net Analyzer ; Programming Enviroment based on Petri Nets ; NuSMV

Course : Protocol Validation [Ref: 214012]

• Year :
• Offered at: Twente
• Contact :J.-P. Katoen
• Topics : Program verification ; CTL ; LTL
• Languages :
• Tools : SPIN ; NuSMV ; UPPAAL

Courses on Ocaml

Course : Formal Methods [Ref : Without a reference name]

• Year : MSc
• Offered at: Beira-Interior
• Contact :S.M. Sousa
• Topics : Hoare Logic ; DMat
• Languages : B-Method ; The CAML Language
• Tools : COQ ; WHY

Course : Theory of Computation [Ref : Without a reference name]

• Year : 3
• Offered at: Beira-Interior
• Contact :S.M. Sousa
• Topics : Functional Programming ; DMat ; Lambda Calculus
• Languages : The CAML Language
• Tools : COQ

Course : Programmation fonctionnelle et preuves [Ref : Without a reference name]

• Year :
• Offered at: Lyon
• Contact :Y. Bertot
• Topics : Functional Programming ; TT ; Lambda Calculus
• Languages : The CAML Language
• Tools : COQ

Courses on OZ

Course : Formal Methods [Ref: CO861]

• Year : MSc
• Offered at: Kent
• Contact :H. Bowman
• Topics : Model Checking
• Languages : Object-Z ; LOTOS
• Tools : CADP

Courses on PEP

Course : Programming Logics III [Ref: ELP-III]

• Year : 3
• Offered at: Minho
• Contact :J.M. ValenÁa
• Topics : Model Checking ; Petri Nets
• Languages :
• Tools : Integrated Net Analyzer ; Programming Enviroment based on Petri Nets ; NuSMV

Courses on PicT^?

Course : Programming Method. IV (Concurrency) [Ref: MP-IV]

• Year : 3
• Offered at: Minho
• Contact :L.S. Barbosa
• Topics : Process Algebras ; Pi-Calculus
• Languages : CCS
• Tools : CWB ; PICT

Courses on Prolog

Course : Programming Languages and Formal Semantics [Ref: dSprog Sem]

• Year :
• Offered at: Aarhus
• Contact :P.D. Mosses
• Topics : Functional Programming ; Formal Semantics
• Languages : Standard ML ; Prolog
• Tools :

Course : Theory of Computation [Ref: TC]

• Year : 4
• Offered at: Porto
• Contact :M. Florido
• Topics : Formal Semantics ; TT ; DMat ; Lambda Calculus
• Languages : Prolog ; Haskell
• Tools :

Courses on PVS

Course : Selected Topics on Software Technology [Ref: AKSWT]

• Year :
• Offered at: Graz
• Contact :P. Lucas
• Topics : Formal program techniques
• Languages :
• Tools : PVS

Courses on RAISEtools

Course : Formal Aspects of Software Engineering I [Ref: 02262]

• Year : S4-S7
• Offered at: Lyngby
• Contact :A. Haxthausen
• Topics :
• Languages : RSL
• Tools : RAISE tools

Course : Formal Aspects of Software Engineering II [Ref: 02268]

• Year : S7-S9
• Offered at: Lyngby
• Contact :D. Bj¯rner
• Topics : Formal Semantics ; Algebraic Semantics
• Languages : RSL
• Tools : RAISE tools

Courses on RAT

Course : Action Semantics and Compiler Generation [Ref: ascg-01]

• Year :
• Offered at: Aarhus
• Contact :P.D. Mosses
• Topics : Action Semantics
• Languages :
• Tools : RAT ; RML ; Actress

Courses on RML

Course : Action Semantics and Compiler Generation [Ref: ascg-01]

• Year :
• Offered at: Aarhus
• Contact :P.D. Mosses
• Topics : Action Semantics
• Languages :
• Tools : RAT ; RML ; Actress

Courses on RSL

Course : Formal Aspects of Software Engineering I [Ref: 02262]

• Year : S4-S7
• Offered at: Lyngby
• Contact :A. Haxthausen
• Topics :
• Languages : RSL
• Tools : RAISE tools

Course : Formal Aspects of Software Engineering II [Ref: 02268]

• Year : S7-S9
• Offered at: Lyngby
• Contact :D. Bj¯rner
• Topics : Formal Semantics ; Algebraic Semantics
• Languages : RSL
• Tools : RAISE tools

Courses on SDL

Course : Distributed Systems [Ref: CO610]

• Year : BSc 3
• Offered at: Kent
• Contact :E.A. Boiten
• Topics :
• Languages : SDL ; E-LOTOS ; Estelle
• Tools :

Course : Formal Methods for Software Engineering [Ref: 213520]

• Year :
• Offered at: Twente
• Contact :E. Brinksma
• Topics : Process Algebras
• Languages : Z-Notation ; FSP ; SDL
• Tools : LTSA ; Z/EVES

Courses on SML

Course : Programming Languages and Formal Semantics [Ref: dSprog Sem]

• Year :
• Offered at: Aarhus
• Contact :P.D. Mosses
• Topics : Functional Programming ; Formal Semantics
• Languages : Standard ML ; Prolog
• Tools :

Course : Software Engineering II [Ref : Without a reference name]

• Year :
• Offered at: Cambridge
• Contact :L.C. Paulson
• Topics : Algorithm refinement
• Languages : Z-Notation ; Standard ML
• Tools :

Course : Functional Programming and Specification [Ref : Without a reference name]

• Year :
• Offered at: Edinburgh
• Contact :D. Sannella
• Topics :
• Languages : Standard ML ; Extended ML
• Tools :

Course : Models and Algorithms [Ref : Without a reference name]

• Year : 2
• Offered at: Nancy
• Contact :D. MÈry
• Topics : Functional Programming ; Formal program techniques
• Languages : Standard ML
• Tools :

Course : Paradigmi di Programmazione [Ref : Without a reference name]

• Year :
• Offered at: Roma
• Contact :P. Cenciarelli
• Topics : Formal Semantics ; Hoare Logic ; TT ; Formal program techniques ; Lambda Calculus ; Polytypism
• Languages : Standard ML
• Tools :

Course : Specification and Verification [Ref : Without a reference name]

• Year :
• Offered at: T.U. M¸nchen
• Contact :T. Nipkow
• Topics : Automated theorem proving ; FOL ; Formal program techniques
• Languages : Standard ML
• Tools : HOL ; Isabelle

Course : Functional programming in Standard ML [Ref : Without a reference name]

• Year : 3/4
• Offered at: Warsaw
• Contact :A. Tarlecki
• Topics : Functional Programming ; Formal Semantics ; FOL ; Formal program techniques ; Lambda Calculus
• Languages : Standard ML ; Haskell
• Tools :

Courses on SPIN

Course : Verification [Ref: V03]

• Year : MSc
• Offered at: Aalborg
• Contact :K.G. Larsen
• Topics : BDD ; CTL ; LTL
• Languages :
• Tools : SPIN ; UPPAAL

Course : Foundations of Systems Development [Ref : Without a reference name]

• Year :
• Offered at: L-M-U M¸nchen
• Contact :M. Wirsing
• Topics : Model Checking ; ADT ; Formal program techniques ; LTL ; TLA
• Languages : Z-Notation
• Tools : CASL ; SPIN

Course : Software engineering II [Ref : Without a reference name]

• Year : 4
• Offered at: Milan Poli.
• Contact :P. San Pietro
• Topics : Model Checking ; Petri Nets
• Languages :
• Tools : SPIN

Course : Software Engineering II [Ref : Without a reference name]

• Year :
• Offered at: Milan Poli.
• Contact :C. Ghezzi
• Topics : Model Checking ; Software Testing
• Languages :
• Tools : SPIN ; Alloy

Course : Specification of Reactive Systems [Ref : Without a reference name]

• Year :
• Offered at: Oldenburg
• Contact :H. Wehrheim
• Topics :
• Languages : CSP
• Tools : FDR ; SPIN

Course : Protocol Validation [Ref: 214012]

• Year :
• Offered at: Twente
• Contact :J.-P. Katoen
• Topics : Program verification ; CTL ; LTL
• Languages :
• Tools : SPIN ; NuSMV ; UPPAAL

Courses on Statecharts

Course : System Analysis - Análisis de Sistemas [Ref: AS]

• Year :
• Offered at: Rosario
• Contact :M. Cristiá
• Topics : Formal Modeling^?
• Languages : Statecharts^? ; Z^? ; TLA^? ; CSP^?
• Tools : Z/EVES

Courses on TLA

Course : System Analysis - Análisis de Sistemas [Ref: AS]

• Year :
• Offered at: Rosario
• Contact :M. Cristiá
• Topics : Formal Modeling^?
• Languages : TLA ; Z^? ; CSP^? ; Statecharts^?
• Tools : Z/EVES

Courses on TRIO

Course : Industrial automation II [Ref : Without a reference name]

• Year : 4/5
• Offered at: Milan Poli.
• Contact :L. Mezzalira
• Topics : Petri Nets
• Languages :
• Tools : TRIO

Course : Formal methods for concurrent and distributed systems [Ref : Without a reference name]

• Year : 4
• Offered at: Milan Poli.
• Contact :D. Mandrioli
• Topics : Hoare Logic ; Temporal Logic ; Refinement in B ; Petri Nets
• Languages : B-Method
• Tools : TRIO

Courses on TrL^?

Course : Program Quality Verification [Ref : Without a reference name]

• Year :
• Offered at: Bologna
• Contact :C. Laneve
• Topics : TT ; Abstract Interpretation
• Languages :
• Tools : T-Logic

Courses on Unity

Course : Advanced System Design [Ref: CO7205]

• Year :
• Offered at: Leicester
• Contact :J. Fiadeiro
• Topics : Software architecture
• Languages : Unity
• Tools : CommUnity

Courses on UPPAAL

Course : Verification [Ref: V03]

• Year : MSc
• Offered at: Aalborg
• Contact :K.G. Larsen
• Topics : BDD ; CTL ; LTL
• Languages :
• Tools : SPIN ; UPPAAL

Course : Semantics and Verification 2002 [Ref: F01-Dat4]

• Year :
• Offered at: Aalborg
• Contact :A. IngÛlfsdÛttir
• Topics : Process Algebras ; BDD
• Languages : CCS
• Tools : CWB ; UPPAAL

Course : Testing and Verification [Ref: TOV04]

• Year :
• Offered at: Aalborg
• Contact :K.G. Larsen
• Topics : Model Checking ; Program verification ; Software Testing
• Languages : MSC
• Tools : UPPAAL

Course : Software Failure and Risk [Ref: CO617]

• Year : BSc 3
• Offered at: Kent
• Contact :R. Lemos
• Topics : Model Checking
• Languages :
• Tools : UPPAAL

Course : Protocol Validation [Ref: 214012]

• Year :
• Offered at: Twente
• Contact :J.-P. Katoen
• Topics : Program verification ; CTL ; LTL
• Languages :
• Tools : SPIN ; NuSMV ; UPPAAL

Courses on VDMSL

Course : Software Technology [Ref: SWT]

• Year : 3
• Offered at: Graz
• Contact :B.K. Aichernig
• Topics : Formal Semantics ; Formal program techniques
• Languages : VDM-SL
• Tools : VDMTools

Course : Formal Methods I [Ref: MFP-I]

• Year : 4
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics : Algebra of Programming ; Formal program techniques ; Mathematics of Program Construction
• Languages : VDM-SL
• Tools : VDMTools

Course : Formal Methods II [Ref: MFP-II]

• Year : 4
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics : Algebra of Programming ; Mathematics of Program Construction ; Data refinement
• Languages : VDM++ ; VDM-SL
• Tools : VDMTools

Course : Formal Methods in Practice [Ref: CSC230]

• Year : 2
• Offered at: Newcastle
• Contact :J. Steggles
• Topics :
• Languages : VDM-SL
• Tools : VDMTools

Course : Formal Specification of Software [Ref: CSC227]

• Year : 2
• Offered at: Newcastle
• Contact :S. Riddle
• Topics :
• Languages : VDM-SL
• Tools : VDMTools

Courses on VDM

Course : Model driven development using VDM++ and UML 1 [Ref: TIVDM1]

• Year : 4 -5
• Offered at: Engineering College of Aarhus
• Contact :P.G. Larsen
• Topics :
• Languages : VDM++
• Tools : VDMTools

Course : Model driven development using VDM++ and UML 2 [Ref: TIVDM1]

• Year : 4 -5
• Offered at: Engineering College of Aarhus
• Contact :P.G. Larsen
• Topics :
• Languages : VDM++
• Tools : VDMTools

Course : Software Technology [Ref: SWT]

• Year : 3
• Offered at: Graz
• Contact :B.K. Aichernig
• Topics : Formal Semantics ; Formal program techniques
• Languages : VDM-SL
• Tools : VDMTools

Course : Formal Methods I [Ref: MFP-I]

• Year : 4
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics :
• Languages : VDM-SL
• Tools : VDMTools

Course : Formal Methods II [Ref: MFP-II]

• Year : 4
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics : Algebra of Programming ; Mathematics of Program Construction ; Data refinement
• Languages : VDM++ ; VDM-SL
• Tools : VDMTools

Course : Formal Methods Laboratory [Ref: LAB-MF]

• Year : 5
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics :
• Languages : B-Method ; VDM++ ; Alloy
• Tools : VDMTools

Course : Formal Methods in Practice [Ref: CSC230]

• Year : 2
• Offered at: Newcastle
• Contact :J. Steggles
• Topics :
• Languages : VDM-SL
• Tools : VDMTools

Course : Formal Specification of Software [Ref: CSC227]

• Year : 2
• Offered at: Newcastle
• Contact :S. Riddle
• Topics :
• Languages : VDM-SL
• Tools : VDMTools

Courses on VPP

Course : Formal Methods II [Ref: MFP-II]

• Year : 4
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics : Algebra of Programming ; Mathematics of Program Construction ; Data refinement
• Languages : VDM++ ; VDM-SL
• Tools : VDMTools

Course : Formal Methods Laboratory [Ref: LAB-MF]

• Year : 5
• Offered at: Minho
• Contact :J.N. Oliveira
• Topics :
• Languages : B-Method ; VDM++ ; Alloy
• Tools : VDMTools

Courses on WHY

Course : Formal Methods [Ref : Without a reference name]

• Year : MSc
• Offered at: Beira-Interior
• Contact :S.M. Sousa
• Topics : Hoare Logic ; DMat
• Languages : B-Method ; The CAML Language
• Tools : COQ ; WHY

Courses on xML

Course : Functional Programming and Specification [Ref : Without a reference name]

• Year :
• Offered at: Edinburgh
• Contact :D. Sannella
• Topics :
• Languages : Standard ML ; Extended ML
• Tools :

Courses on Z

Course : Formal Specification [Ref: MSH1012]

• Year : 3
• Offered at: Anglia
• Contact :N. Dean
• Topics :
• Languages : Z-Notation