|
Ref
|
Y/S
|
Module
|
Institution
|
Contact
|
Topics/Langs/Tools
|
|---|
|
MSH1012
|
3
|
Formal Specification
|
Anglia
|
N. Dean
|
Z
|
|
|
MSc
|
Formal Methods
|
Beira-Interior
|
S.M. Sousa
|
B
,
Coq
,
DMat
,
HL
,
Ocaml
,
WHY
|
|
|
5/ MSc
|
Specification and Formal Verification in B
|
Bordeaux
|
G.Sutre
|
ARef
,
AtelierB
,
B
,
Btlk
,
PV
|
|
|
|
Software Engineering II
|
Cambridge
|
L.C. Paulson
|
ARef
,
SML
,
Z
|
|
4ICT8
|
|
System Modelling and Specification
|
Dublin
|
A. Hughes
|
Haskell
,
IVDM
,
IVDMH
,
MPC
|
|
4BA1
|
|
Information Systems (part II)
|
Dublin
|
M. Airchinnigh
|
FS
,
IVDM
,
MPC
|
|
ELINFO 01A00062
|
1
|
Formal Methods in Systems Modeling
|
Gent
|
R.T. Boute
|
AoP
,
FPT
|
|
FP1
|
1
|
Further Programming 1
|
Glasgow
|
R. Irving
|
FPT
|
|
SWT
|
3
|
Software Technology
|
Graz
|
B.K. Aichernig
|
FPT
,
FS
,
VDMSL
,
VDMT
|
|
AKSWT
|
|
Selected Topics on Software Technology
|
Graz
|
P. Lucas
|
FPT
,
PVS
|
|
141@
|
1
|
Reasoning about Programs
|
Imperial C.
|
K. Broda
|
FPT
|
|
475
|
|
Software Engineering Environments
|
Imperial C.
|
M. Huth
|
Alloy
,
FPT
|
|
302
|
|
Software Engineering - Methods
|
Imperial C.
|
M. Huth
|
Alloy
,
FPT
|
|
CO508
|
BSc 2
|
Software and Systems Design
|
Kent
|
R. Lemos
|
CADiZ
,
Z
|
|
CO515
|
BSc 2
|
Theory of Computer Science
|
Kent
|
J. Derrick
|
FOL
,
FP
,
FPT
,
Z
|
|
CO861
|
MSc
|
Formal Methods
|
Kent
|
H. Bowman
|
CADP
,
LOTOS
,
MC
,
OZ
|
|
CS03PV
|
3
|
Program Verification and Specification
|
London (K.C.)
|
D. Clark
|
B
,
MC
,
PV
|
|
02262
|
S4-S7
|
Formal Aspects of Software Engineering I
|
Lyngby
|
A. Haxthausen
|
RAISEtools
,
RSL
|
|
02268
|
S7-S9
|
Formal Aspects of Software Engineering II
|
Lyngby
|
D. Bjørner
|
ASe
,
FS
,
RAISEtools
,
RSL
|
|
|
4
|
Software Engineering
|
Lisbon
|
R.G. Crespo
|
LOTOS
,
Z
|
|
CS1112
|
1
|
Reasoning about Programs
|
Manchester
|
K. Lau
|
FOL
,
FPT
|
|
|
MSc
|
Techniques de preuve et vérification formelle
|
Marseille
|
J.-R. Abrial
|
ASM
,
B
,
MC
|
|
|
MSc
|
Méthodes Formelles
|
Metz
|
D. Cansell
|
B
,
FPT
|
|
|
4
|
Formal methods for concurrent and distributed systems
|
Milan Poli.
|
D. Mandrioli
|
B
,
HL
,
Petri
,
RefB
,
TL
,
TRIO
|
|
|
|
Software Engineering II
|
Milan Poli.
|
C. Ghezzi
|
Alloy
,
MC
,
SPIN
,
TFM
|
|
MFP-I
|
4
|
Formal Methods I
|
Minho
|
J.N. Oliveira
|
AoP
,
FPT
,
MPC
,
VDMSL
,
VDMT
|
|
MFP-II
|
4
|
Formal Methods II
|
Minho
|
J.N. Oliveira
|
AoP
,
DRef
,
MPC
,
VDMSL
,
VDMT
,
VPP
|
|
LAB-MF
|
5
|
Formal Methods Laboratory
|
Minho
|
J.N. Oliveira
|
Alloy
,
B
,
VDMT
,
VPP
|
|
|
|
Specification and Verification
|
T.U. München
|
T. Nipkow
|
ATP
,
FOL
,
FPT
,
HOL
,
Isabelle
,
SML
|
|
|
|
Foundations of Systems Development
|
L-M-U München
|
M. Wirsing
|
ADT
,
CASL
,
FPT
,
LTL
,
MC
,
SPIN
,
TLA
,
Z
|
|
|
5/ MSc
|
Inform. Syst. Specification and Modelling
|
Nancy
|
D. Méry
|
B
,
DMat
|
|
|
2
|
Models and Algorithms
|
Nancy
|
D. Méry
|
FP
,
FPT
,
SML
|
|
MSF-CA
|
MSc
|
Model-Oriented Formal Methods
|
Nantes
|
J.C. Attiogbé
|
AtelierB
,
B
,
Z
,
ZANS
,
ZEVES
,
ZTC
|
|
|
|
Méthode de spécification formelle B
|
Nantes
|
H. Habrias
|
B
|
|
IFM-CA
|
MSc 1-2
|
Formal Methods Integration
|
Nantes
|
J.C. Attiogbé
|
B
,
CCS
,
CSP
,
MPS
,
PA
|
|
CSC227
|
2
|
Formal Specification of Software
|
Newcastle
|
S. Riddle
|
VDMSL
,
VDMT
|
|
CSC230
|
2
|
Formal Methods in Practice
|
Newcastle
|
J. Steggles
|
VDMSL
,
VDMT
|
|
SEM
|
M
|
Software Engineering Mathematics
|
Oxford
|
A. Martin
|
DMat
,
Z
|
|
SDE
|
M
|
Specification and Design
|
Oxford
|
A. Martin
|
FuZZ
,
Z
|
|
ASD
|
M
|
Advanced Software Development
|
Oxford
|
J. Davies
|
DRef
,
RC
,
Z
|
|
MAS
|
M
|
Machine-Assisted Software Engineering
|
Oxford
|
J. Davies
|
B
,
Btlk
|
|
MF
|
5
|
Méthodes Formelles de spécification des Systèmes Informatiques
|
Paris (ENST)
|
S. Vignes
|
B
,
Z
|
|
|
4/5
|
Spécifications Formelles
|
Poitiers
|
E. Andres (contact)
|
B
,
FPT
,
FS
|
|
|
|
Paradigmi di Programmazione
|
Roma
|
P. Cenciarelli
|
FPT
,
FS
,
HL
,
LamC
,
PolyT
,
SML
,
TT
|
|
CM140
|
1
|
Introduction to Formal Methods
|
Southampton
|
M.J. Butler
|
PV
,
Z
,
ZTC
|
|
EL208
|
2
|
Z Specification Design Exercise
|
Southampton
|
M.J. Butler
|
Z
,
ZTC
|
|
CM314
|
3
|
Critical Systems
|
Southampton
|
M.J. Butler
|
B
,
Btlk
,
RefB
,
Safety
|
|
CS L3
|
S2
|
Systems and Software Engineering
|
London (S.B.)
|
A. Abdallah
|
CSP
,
Haskell
,
Z
|
|
31P6
|
|
Software Engineering II
|
Stirling
|
S. Maharaj
|
Z
|
|
213520
|
|
Formal Methods for Software Engineering
|
Twente
|
E. Brinksma
|
FSP
,
LTSA
,
PA
,
SDL
,
Z
,
ZEVES
|
|
|
3/4
|
Functional programming in Standard ML
|
Warsaw
|
A. Tarlecki
|
FOL
,
FP
,
FPT
,
FS
,
Haskell
,
LamC
,
SML
|
|
37-483
|
S1
|
Introd. to high-level system design and analysis
|
Zuerich
|
R.F. Staerk
|
ASM
|
