|
Ref
|
Y/S
|
Module
|
Institution
|
Contact
|
Topics/Langs/Tools
|
|---|
|
V03
|
MSc
|
Verification
|
Aalborg
|
K.G. Larsen
|
BDD
,
CTL
,
LTL
,
SPIN
,
UPPAAL
|
|
|
3
|
Theory of Computation
|
Beira-Interior
|
S.M. Sousa
|
Coq
,
DMat
,
FP
,
LamC
,
Ocaml
|
|
|
MSc
|
Formal Methods
|
Beira-Interior
|
S.M. Sousa
|
B
,
Coq
,
DMat
,
HL
,
Ocaml
,
WHY
|
|
|
|
Temporal and Modal Logics for Parallelism and security
|
Bremen
|
L. Schröder
|
PA
,
TL
|
|
FORMEL
|
S7
|
Methodes formelles, verification, model checking
|
Brest
|
L. Marcé
|
CTL
,
LTL
,
Lotrec
,
MC
|
|
3ICT5
|
|
Mathematical Modelling
|
Dublin
|
M. Tyrrell
|
AL
,
LamC
,
PA
,
PiC
|
|
CO515
|
BSc 2
|
Theory of Computer Science
|
Kent
|
J. Derrick
|
FOL
,
FP
,
FPT
,
Z
|
|
CS2APL
|
|
Applied Logic
|
London (K.C.)
|
M. Zakharyaschev
|
CTL
|
|
CSMMTL
|
|
Modal and Temporal Logics
|
London (K.C.)
|
A. Kurucz
|
TL
|
|
|
|
Programmation fonctionnelle et preuves
|
Lyon
|
Y. Bertot
|
Coq
,
FP
,
LamC
,
Ocaml
,
TT
|
|
CS1112
|
1
|
Reasoning about Programs
|
Manchester
|
K. Lau
|
FOL
,
FPT
|
|
|
4
|
Formal methods for concurrent and distributed systems
|
Milan Poli.
|
D. Mandrioli
|
B
,
HL
,
Petri
,
RefB
,
TL
,
TRIO
|
|
702752
|
2
|
Programming Logics II
|
Minho
|
J.B. Almeida
|
LamC
,
TT
|
|
|
|
Specification and Verification
|
T.U. München
|
T. Nipkow
|
ATP
,
FOL
,
FPT
,
HOL
,
Isabelle
,
SML
|
|
|
|
Programming Language Semantics
|
T.U. München
|
T. Nipkow
|
ATP
,
FS
,
HL
,
Isabelle
,
TT
|
|
|
|
Foundations of Systems Development
|
L-M-U München
|
M. Wirsing
|
ADT
,
CASL
,
FPT
,
LTL
,
MC
,
SPIN
,
TLA
,
Z
|
|
|
MSc
|
Méthodes Formelles et Fiabilité des Systèmes Embarqués
|
Nice
|
M. Auguin (contact)
|
BDD
,
MC
,
PV
,
TL
|
|
LC
|
|
Lambda Calculus
|
Oxford
|
A. Ker
|
FP
,
LamC
|
|
TC
|
4
|
Theory of Computation
|
Porto
|
M. Florido
|
DMat
,
FS
,
Haskell
,
LamC
,
Prolog
,
TT
|
|
|
|
Logics and Verification
|
Paris VII
|
P. Habermehl
|
BDD
,
BDDC
,
MC
,
TL
|
|
|
|
Foundations of Informatics: Semantics II
|
Pisa
|
U. Montanari
|
LamC
,
TT
|
|
|
|
Paradigmi di Programmazione
|
Roma
|
P. Cenciarelli
|
FPT
,
FS
,
HL
,
LamC
,
PolyT
,
SML
,
TT
|
|
|
MSc
|
Spécifications formelles, connaissances et raisonnement
|
Strasbourg
|
P. Gancarski (contact)
|
Coq
,
LamC
,
PV
|
|
|
|
Foundations of Informatics (semantics)
|
Torino
|
M. Ciancaglini
|
FS
,
LamC
,
TT
|
|
214012
|
|
Protocol Validation
|
Twente
|
J.-P. Katoen
|
CTL
,
LTL
,
NuSMV
,
PV
,
SPIN
,
UPPAAL
|
|
|
3/4
|
Functional programming in Standard ML
|
Warsaw
|
A. Tarlecki
|
FOL
,
FP
,
FPT
,
FS
,
Haskell
,
LamC
,
SML
|
|
|
|
Semantics and Specifications
|
Warsaw
|
A. Tarlecki
|
FS
,
HL
|
