FME Review of Education Resources
[ FME ]

[ In Europe | Outside Europe ]

• Last update: 2004.05.14.
• Currently: 117 modules.
• Review performed by: FME-SOE
• E-mail: education@fmeurope.org.

  In Europe

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

  Year/Level:
  Contact:	P.D. Mosses
  Offered at:	Aarhus
  Topics:	Action Semantics
  Languages/tools:	Actress ; RAT ; RML

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

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

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

  Year/Level:
  Contact:	A. Ingólfsdóttir
  Offered at:	Aalborg
  Topics:	BDD ; Process Algebras
  Languages/tools:	CCS ; UPPAAL ; CWB

• Testing and Verification   [Ref: TOV04]

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

• Verification   [Ref: V03]

  Year/Level:	MSc
  Contact:	K.G. Larsen
  Offered at:	Aalborg
  Topics:	LTL ; CTL ; BDD
  Languages/tools:	SPIN ; UPPAAL

• Formal Specification   [Ref: MSH1012]

  Year/Level:	3
  Contact:	N. Dean
  Offered at:	Anglia
  Topics:
  Languages/tools:	Z-Notation

• Theory of Computation   [Ref: ]

  Year/Level:	3
  Contact:	S.M. Sousa
  Offered at:	Beira-Interior
  Topics:	; Functional Programming ; DMat
  Languages/tools:	The CAML Language ; COQ

• Formal Methods   [Ref: ]

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

• Formal Modelling and Process-oriented Systems   [Ref: ]

  Year/Level:
  Contact:	J. Padberg
  Offered at:	Berlin
  Topics:	Petri Nets
  Languages/tools:

• Program Quality Verification   [Ref: ]

  Year/Level:
  Contact:	C. Laneve
  Offered at:	Bologna
  Topics:	Abstract Interpretation ; TT
  Languages/tools:	T-Logic

• Specification and Formal Verification in B   [Ref: ]

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

• Formal Methods in Software Engineering   [Ref: ]

  Year/Level:
  Contact:	A. Griffault
  Offered at:	Bordeaux
  Topics:
  Languages/tools:

• Formal Specifications   [Ref: ]

  Year/Level:
  Contact:	A. Griffault
  Offered at:	Bordeaux
  Topics:
  Languages/tools:

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

  Year/Level:
  Contact:	T. Mossakowski
  Offered at:	Bremen
  Topics:	Functional Programming ; Algebra of Programming
  Languages/tools:	Haskell

• Techniques of Correct Software Development   [Ref: TEKS]

  Year/Level:
  Contact:	C. Lüth
  Offered at:	Bremen
  Topics:	ADT ; Model Checking
  Languages/tools:	CSP ; CASL ; Isabelle ; FDR

• Algebraic Specification   [Ref: ]

  Year/Level:
  Contact:	L. Schröder
  Offered at:	Bremen
  Topics:	ADT
  Languages/tools:	CASL

• Semantics of Programming Languages   [Ref: ]

  Year/Level:
  Contact:	L. Schröder
  Offered at:	Bremen
  Topics:	Formal Semantics
  Languages/tools:

• Systems, Automata, and Coalgebras   [Ref: ]

  Year/Level:
  Contact:	L. Schröder
  Offered at:	Bremen
  Topics:	Process Algebras
  Languages/tools:	CCS

• Temporal and Modal Logics for Parallelism and security   [Ref: ]

  Year/Level:
  Contact:	L. Schröder
  Offered at:	Bremen
  Topics:	Temporal Logic ; Process Algebras
  Languages/tools:

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

  Year/Level:	S7
  Contact:	L. Marcé
  Offered at:	Brest
  Topics:	LTL ; CTL ; Model Checking
  Languages/tools:	LOTREC

• Software Engineering II   [Ref: ]

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

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

  Year/Level:
  Contact:	Horst Reichel
  Offered at:	T.U. Dresden
  Topics:	ADT ; Process Algebras
  Languages/tools:	CASL

• System Modelling and Specification   [Ref: 4ICT8]

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

• Mathematical Modelling   [Ref: 3ICT5]

  Year/Level:
  Contact:	M. Tyrrell
  Offered at:	Dublin
  Topics:	; Process Algebras ; Algorithms and Complexity ; Pi-Calculus
  Languages/tools:

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

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

• Functional Programming and Specification   [Ref: ]

  Year/Level:
  Contact:	D. Sannella
  Offered at:	Edinburgh
  Topics:
  Languages/tools:	Standard ML ; Extended ML

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

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

• Introduction to Formal Methods   [Ref: 2R440]

  Year/Level:	4
  Contact:	J. Baeten
  Offered at:	Eindhoven
  Topics:
  Languages/tools:

• Process Algebra   [Ref: 2M920]

  Year/Level:	2/3
  Contact:	J. Baeten
  Offered at:	Eindhoven
  Topics:	Process Algebras
  Languages/tools:

• Proving with Computer Assistance   [Ref: 2IF40]

  Year/Level:	4.2
  Contact:	R. Nederpelt
  Offered at:	Eindhoven
  Topics:	Automated theorem proving
  Languages/tools:

• Formal Methods in Systems Modeling   [Ref: ELINFO 01A00062]

  Year/Level:	1
  Contact:	R.T. Boute
  Offered at:	Gent
  Topics:	Algebra of Programming ; Formal program techniques
  Languages/tools:

• Further Programming 1   [Ref: FP1]

  Year/Level:	1
  Contact:	R. Irving
  Offered at:	Glasgow
  Topics:	Formal program techniques
  Languages/tools:

• Software Technology   [Ref: SWT]

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

• Selected Topics on Software Technology   [Ref: AKSWT]

  Year/Level:
  Contact:	P. Lucas
  Offered at:	Graz
  Topics:	Formal program techniques
  Languages/tools:	PVS

• Reasoning about Programs   [Ref: 141@]

  Year/Level:	1
  Contact:	K. Broda
  Offered at:	Imperial C.
  Topics:	Formal program techniques
  Languages/tools:

• Software Engineering Environments   [Ref: 475]

  Year/Level:
  Contact:	M. Huth
  Offered at:	Imperial C.
  Topics:	Formal program techniques
  Languages/tools:	Alloy

• Software Engineering - Methods   [Ref: 302]

  Year/Level:
  Contact:	M. Huth
  Offered at:	Imperial C.
  Topics:	Formal program techniques
  Languages/tools:	Alloy

• Software and Systems Design   [Ref: CO508]

  Year/Level:	BSc 2
  Contact:	R. Lemos
  Offered at:	Kent
  Topics:
  Languages/tools:	Z-Notation ; CADiZ

• Theory of Computer Science   [Ref: CO515]

  Year/Level:	BSc 2
  Contact:	J. Derrick
  Offered at:	Kent
  Topics:	Functional Programming ; Formal program techniques ; FOL
  Languages/tools:	Z-Notation

• Distributed Systems   [Ref: CO610]

  Year/Level:	BSc 3
  Contact:	E.A. Boiten
  Offered at:	Kent
  Topics:
  Languages/tools:	E-LOTOS ; Estelle ; SDL

• Software Failure and Risk   [Ref: CO617]

  Year/Level:	BSc 3
  Contact:	R. Lemos
  Offered at:	Kent
  Topics:	Model Checking
  Languages/tools:	UPPAAL

• Formal Methods   [Ref: CO861]

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

• Advanced System Design   [Ref: CO7205]

  Year/Level:
  Contact:	J. Fiadeiro
  Offered at:	Leicester
  Topics:	Software architecture
  Languages/tools:	Unity ; CommUnity

• Program Verification and Specification   [Ref: CS03PV]

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

• Introduction to the Theory of Computation   [Ref: CS1ITC]

  Year/Level:
  Contact:	A. Kurucz
  Offered at:	London (K.C.)
  Topics:
  Languages/tools:

• Applied Logic   [Ref: CS2APL]

  Year/Level:
  Contact:	M. Zakharyaschev
  Offered at:	London (K.C.)
  Topics:	CTL
  Languages/tools:

• Modal and Temporal Logics   [Ref: CSMMTL]

  Year/Level:
  Contact:	A. Kurucz
  Offered at:	London (K.C.)
  Topics:	Temporal Logic
  Languages/tools:

• Formal Methods   [Ref: ]

  Year/Level:
  Contact:	D. Buchs
  Offered at:	Lausanne
  Topics:	ADT
  Languages/tools:

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

  Year/Level:	S4-S7
  Contact:	A. Haxthausen
  Offered at:	Lyngby
  Topics:
  Languages/tools:	RSL ; RAISE tools

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

  Year/Level:	S7-S9
  Contact:	D. Bjørner
  Offered at:	Lyngby
  Topics:	Formal Semantics ; Algebraic Semantics
  Languages/tools:	RSL ; RAISE tools

• Software Engineering   [Ref: ]

  Year/Level:	4
  Contact:	R.G. Crespo
  Offered at:	Lisbon
  Topics:
  Languages/tools:	Z-Notation ; LOTOS

• Programmation fonctionnelle et preuves   [Ref: ]

  Year/Level:
  Contact:	Y. Bertot
  Offered at:	Lyon
  Topics:	; TT ; Functional Programming
  Languages/tools:	The CAML Language ; COQ

• Reasoning about Programs   [Ref: CS1112]

  Year/Level:	1
  Contact:	K. Lau
  Offered at:	Manchester
  Topics:	FOL ; Formal program techniques
  Languages/tools:

• Techniques de preuve et vérification formelle   [Ref: ]

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

• Méthodes Formelles   [Ref: ]

  Year/Level:	MSc
  Contact:	D. Cansell
  Offered at:	Metz
  Topics:	Formal program techniques
  Languages/tools:	B-Method

• Formal methods for concurrent and distributed systems   [Ref: ]

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

• Software engineering II   [Ref: ]

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

• Industrial automation II   [Ref: ]

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

• Software Engineering II   [Ref: ]

  Year/Level:
  Contact:	C. Ghezzi
  Offered at:	Milan Poli.
  Topics:	Model Checking ; Software Testing
  Languages/tools:	Alloy ; SPIN

• Programming Methodology I   [Ref: MP-I]

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

• Programming Logics II   [Ref: 702752]

  Year/Level:	2
  Contact:	J.B. Almeida
  Offered at:	Minho
  Topics:	; TT
  Languages/tools:

• Programming Logics III   [Ref: ELP-III]

  Year/Level:	3
  Contact:	J.M. Valença
  Offered at:	Minho
  Topics:	Petri Nets ; Model Checking
  Languages/tools:	NuSMV ; Integrated Net Analyzer

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

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

• Formal Methods I   [Ref: MFP-I]

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

• Formal Methods II   [Ref: MFP-II]

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

• Formal Methods Laboratory   [Ref: LAB-MF]

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

• Specification and Verification   [Ref: ]

  Year/Level:
  Contact:	T. Nipkow
  Offered at:	T.U. München
  Topics:	FOL ; Formal program techniques ; Automated theorem proving
  Languages/tools:	Standard ML ; Isabelle ; HOL

• Programming Language Semantics   [Ref: ]

  Year/Level:
  Contact:	T. Nipkow
  Offered at:	T.U. München
  Topics:	Formal Semantics ; TT ; Hoare Logic ; Automated theorem proving
  Languages/tools:	Isabelle

• Foundations of Systems Development   [Ref: ]

  Year/Level:
  Contact:	M. Wirsing
  Offered at:	L-M-U München
  Topics:	ADT ; Formal program techniques ; TLA ; LTL ; Model Checking
  Languages/tools:	Z-Notation ; SPIN ; CASL

• Inform. Syst. Specification and Modelling   [Ref: ]

  Year/Level:	5/ MSc
  Contact:	D. Méry
  Offered at:	Nancy
  Topics:	DMat
  Languages/tools:	B-Method

• Models and Algorithms   [Ref: ]

  Year/Level:	2
  Contact:	D. Méry
  Offered at:	Nancy
  Topics:	Formal program techniques ; Functional Programming
  Languages/tools:	Standard ML

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

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

• Méthode de spécification formelle B   [Ref: ]

  Year/Level:
  Contact:	H. Habrias
  Offered at:	Nantes
  Topics:
  Languages/tools:	B-Method

• Formal Methods Integration   [Ref: IFM-CA]

  Year/Level:	MSc 1-2
  Contact:	J.C. Attiogbé
  Offered at:	Nantes
  Topics:	Multi-paradigm Specifications ; Process Algebras
  Languages/tools:	CCS ; CSP ; B-Method

• Formal Specification of Software   [Ref: CSC227]

  Year/Level:	2
  Contact:	S. Riddle
  Offered at:	Newcastle
  Topics:
  Languages/tools:	VDM-SL ; VDMTools

• Formal Methods in Practice   [Ref: CSC230]

  Year/Level:	2
  Contact:	J. Steggles
  Offered at:	Newcastle
  Topics:
  Languages/tools:	VDM-SL ; VDMTools

• Méthodes Formelles et Fiabilité des Systèmes Embarqués   [Ref: ]

  Year/Level:	MSc
  Contact:	M. Auguin (contact)
  Offered at:	Nice
  Topics:	BDD ; Temporal Logic ; Model Checking ; Program verification
  Languages/tools:

• Mathematics of Program Construction   [Ref: G51MPC]

  Year/Level:	1
  Contact:	R. Backhouse
  Offered at:	Nottingham
  Topics:	Mathematics of Program Construction
  Languages/tools:

• Programming Algebra   [Ref: G53PAL]

  Year/Level:	3
  Contact:	R. Backhouse
  Offered at:	Nottingham
  Topics:	Algebra of Programming ; Fixed Point Calculus ; Polytypism
  Languages/tools:

• Specification of Reactive Systems   [Ref: ]

  Year/Level:
  Contact:	H. Wehrheim
  Offered at:	Oldenburg
  Topics:
  Languages/tools:	CSP ; SPIN ; FDR

• Formal Program Design I   [Ref: FPD-I]

  Year/Level:
  Contact:	G. Jones
  Offered at:	Oxford
  Topics:	Algorithm refinement
  Languages/tools:

• Formal Program Design II   [Ref: FPD-II]

  Year/Level:
  Contact:	R. Bird
  Offered at:	Oxford
  Topics:	Data refinement
  Languages/tools:

• Lambda Calculus   [Ref: LC]

  Year/Level:
  Contact:	A. Ker
  Offered at:	Oxford
  Topics:	; Functional Programming
  Languages/tools:

• Application-Oriented Program Semantics   [Ref: AOPS]

  Year/Level:
  Contact:	J. Sanders
  Offered at:	Oxford
  Topics:	Formal Semantics
  Languages/tools:

• Domain Theory   [Ref: DTS]

  Year/Level:
  Contact:	G.M. Reed
  Offered at:	Oxford
  Topics:	Domains ; Pi-Calculus
  Languages/tools:

• Software Engineering Mathematics   [Ref: SEM]

  Year/Level:	M
  Contact:	A. Martin
  Offered at:	Oxford
  Topics:	DMat
  Languages/tools:	Z-Notation

• Specification and Design   [Ref: SDE]

  Year/Level:	M
  Contact:	A. Martin
  Offered at:	Oxford
  Topics:
  Languages/tools:	Z-Notation ; FuZZ

• Advanced Software Development   [Ref: ASD]

  Year/Level:	M
  Contact:	J. Davies
  Offered at:	Oxford
  Topics:	Refinement Calculus ; Data refinement
  Languages/tools:	Z-Notation

• Machine-Assisted Software Engineering   [Ref: MAS]

  Year/Level:	M
  Contact:	J. Davies
  Offered at:	Oxford
  Topics:
  Languages/tools:	B-Method ; B-Toolkit

• Concurrency and Distributed Systems   [Ref: CDS]

  Year/Level:	M
  Contact:	J. Davies
  Offered at:	Oxford
  Topics:
  Languages/tools:	CSP ; FDR

• Advanced Concurrency Tools   [Ref: ACT]

  Year/Level:	M
  Contact:	J. Davies
  Offered at:	Oxford
  Topics:
  Languages/tools:	CSP ; FDR

• Functional Programming   [Ref: FPR]

  Year/Level:	M
  Contact:	J. Gibbons
  Offered at:	Oxford
  Topics:	Functional Programming
  Languages/tools:	Haskell ; Hugs ; Gofer

• Theory of Computation   [Ref: TC]

  Year/Level:	4
  Contact:	M. Florido
  Offered at:	Porto
  Topics:	; Formal Semantics ; DMat ; TT
  Languages/tools:	Haskell ; Prolog

• Logics and Verification   [Ref: ]

  Year/Level:
  Contact:	P. Habermehl
  Offered at:	Paris VII
  Topics:	BDD ; Model Checking ; Temporal Logic
  Languages/tools:	BBDC

• Méthodes Formelles de spécification des Systèmes Informatiques   [Ref: MF]

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

• Foundations of Abtract Interpretation   [Ref: ]

  Year/Level:	MSc
  Contact:	P. Cousot
  Offered at:	Paris VII (et al)
  Topics:	Abstract Interpretation
  Languages/tools:

• Verification of infinite systems   [Ref: ]

  Year/Level:	MSc
  Contact:	P. Schnoebelen
  Offered at:	Paris VII (et al)
  Topics:	Petri Nets ; Program verification
  Languages/tools:

• Foundations of Informatics: Semantics A   [Ref: ]

  Year/Level:
  Contact:	U. Montanari
  Offered at:	Pisa
  Topics:	Formal Semantics
  Languages/tools:

• Foundations of Informatics: Semantics II   [Ref: ]

  Year/Level:
  Contact:	U. Montanari
  Offered at:	Pisa
  Topics:	TT ;
  Languages/tools:

• Spécifications Formelles   [Ref: ]

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

• Formal methods in informatics   [Ref: ]

  Year/Level:
  Contact:	A. Labella
  Offered at:	Roma
  Topics:	Algebraic Semantics ; Fixed Point Calculus ; Domains
  Languages/tools:

• Paradigmi di Programmazione   [Ref: ]

  Year/Level:
  Contact:	P. Cenciarelli
  Offered at:	Roma
  Topics:	Hoare Logic ; ; TT ; Polytypism ; Formal program techniques ; Formal Semantics
  Languages/tools:	Standard ML

• Introduction to Formal Methods   [Ref: CM140]

  Year/Level:	1
  Contact:	M.J. Butler
  Offered at:	Southampton
  Topics:	Program verification
  Languages/tools:	Z-Notation ; ZTC

• Z Specification Design Exercise   [Ref: EL208]

  Year/Level:	2
  Contact:	M.J. Butler
  Offered at:	Southampton
  Topics:
  Languages/tools:	Z-Notation ; ZTC

• Critical Systems   [Ref: CM314]

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

• Systems and Software Engineering   [Ref: CS L3]

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

• Software Engineering II   [Ref: 31P6]

  Year/Level:
  Contact:	S. Maharaj
  Offered at:	Stirling
  Topics:
  Languages/tools:	Z-Notation

• Spécifications formelles, connaissances et raisonnement   [Ref: ]

  Year/Level:	MSc
  Contact:	P. Gancarski (contact)
  Offered at:	Strasbourg
  Topics:	; Program verification
  Languages/tools:	COQ

• Foundations of Informatics (semantics)   [Ref: ]

  Year/Level:
  Contact:	M. Ciancaglini
  Offered at:	Torino
  Topics:	Formal Semantics ; ; TT
  Languages/tools:

• Modélisation et analyse des systèmes à événements discrets   [Ref: ]

  Year/Level:
  Contact:	Robert Valette
  Offered at:	Toulouse
  Topics:	Petri Nets
  Languages/tools:

• Formal Methods for Software Engineering   [Ref: 213520]

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

• Protocol Validation   [Ref: 214012]

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

• Functional programming in Standard ML   [Ref: ]

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

• Semantics and Specifications   [Ref: ]

  Year/Level:
  Contact:	A. Tarlecki
  Offered at:	Warsaw
  Topics:	Formal Semantics ; Hoare Logic
  Languages/tools:

• Design of Information Structures   [Ref: CS126]

  Year/Level:	1
  Contact:	S. Russ
  Offered at:	Warwick
  Topics:	ADT
  Languages/tools:

• Formal Methods in Software Engineering   [Ref: MFIEng]

  Year/Level:	5
  Contact:	M. Alpuente
  Offered at:	Univ. Polit. Valencia
  Topics:	Program verification ; Model Checking
  Languages/tools:

• Introd. to high-level system design and analysis   [Ref: 37-483]

  Year/Level:	S1
  Contact:	R.F. Staerk
  Offered at:	Zuerich
  Topics:	Abstract State Machines
  Languages/tools:

  Outside Europe

• See Formal Methods Education Resources (which also includes European courses)