Formal Methods Europe Logo Formal Methods Europe
   
   
 
 Formal Methods

  Choosing
  Methods
  Tools
  Applications
  FAQs
  Literature
  Journals
  Education
  Projects
  Universities
  Industry
  Groups
  Links
 

A Survey of Formal Methods Courses in European Higher Education

The FME Subgroup on Education
(Convenor: J.N. Oliveira)
education@fmeurope.org

Accepted for presentation at the
COLOGNET/FORMAL METHODS EUROPE SYMPOSIUM ON TEACHING FORMAL METHODS 2004,
Ghent University, Belgium, Nov 18-19, 2004

Abstract:

This paper presents a survey of Formal Methods courses in European higher education carried out by the FME Subgroup on Education over the last two years. The survey data sample is made of 117 courses spreading over 58 higher-education institutions across 13 European countries and involving (at least) 91 academic staff.

A total number of 365 websites have been browsed which are accessible from the electronic (HTML) version of this paper in the form of links to course websites, lecturers and topic entries in encyclopedias or virtual libraries.

Three main projections of our sample are briefly analysed. Although far from being fully representative, these already provide some useful indicators about the impact of formal methods in European computing curricula.


Contents

Introduction

In March 2001 the FME association created the FME Subgroup on Education (hereafter abbreviated to FME-SoE) targeted at developing and recommending curricular guidelines for formal method (FM) teaching at undergraduate level. In its aims and motivation, the initiative can be regarded as a «FM replica» of the Computing Curricula 2001 (hereafter abbreviated to CC2001) proposed by the ACM/IEEE Computer JointTask Force on Computing Curricula [12].

Despite the significant advances in FMs over the last decades, both at foundational or tool support level [*], the only explicit reference to the subject in [12] is elective unit SE10 of the Software Engineering area, modestly consisting of the following topics:

  • Formal methods concepts
  • Formal specification languages
  • Executable and non-executable specifications
  • Pre and post assertions
  • Formal verification

Are formal methods altogether so irrelevant? When CC2001 was released (end of 2001), some may have felt that the curricula were biased towards the pragmatism of US higher education, arguing that different approaches could be found elsewhere, notably in Europe. This viewpoint had in fact been expressed, some years earlier, by J. Cuadrado [3] who -- in such a widespread journal as the BYTE MAGAZINE -- criticized US curricula for lack of mathematical support for FM-based software design courses. However, the planned structure of the CC2001 report included 3 more volumes: one on Computer Engineering, another on Information Systems and another one on Software Engineering.

The last draft of latter was released in February 2004, hereafter referred to as the SEEK report [13]. This report offers a broad and more eclectic body of knowledge, in particular exhibiting a far more expressive FM-component:

CMP.fm.1 --
Application of abstract machines (eg. Paisely, SDL)
CMP.fm.2 --
Application of specification languages and methods (eg. ASM, B, CSP, VDM, Z)
CMP.fm.3 --
Automatic generation of code from a specification
CMP.fm.4 --
Program derivation
CMP.fm.5 --
Analysis of candidate implementations
CMP.fm.6 --
Mapping a specification to different implementations
CMP.fm.7 --
Refinement
CMP.fm.8 --
Proofs of correctness
FND.mf.11 --
Algebraic structures
MAA.md.2 --
Pre & post conditions, invariants
MAA.md.3 --
Introduction to mathematical models and specification languages (Z, VDM)
MAA.md.4 --
Model checking and development tools
MAA.md.5 --
Properties of modelling languages
MAA.md.6 --
Syntax vs semantics (understanding model representations)
MAA.tm.4 --
Domain modelling
MAA.rsd.3 --
Spec. languages (eg. structured English, UML, formal lang. such as Z, VDM, SCR, RSML, etc)
DES.nst.6 --
Formal design analysis
EVO.ac.7 --
Program transformation

That this collection of topics is still incomplete can be checked by looking at the (long) list of individual notations, methods and tools of [2]. However, the questions arise: which of these methods are mature enough to reach every school desk? Can newcomers trust them and embark on embodying them in their (FM-specific or other) curricula? Because its main purpose is to support research, the information available from [2] is not structured as an educational body of knowledge and so it does not provide an effective answer to the questions raised above.

This has motivated FME-SoE to perform a survey of existing courses which actually adopt and teach such methods. The main purpose of this paper is to publish a summary of this survey, thus closing what has been regarded as the starting point of FME-SoE's activity. This summary includes some preliminary conclusions about the collected data.

When the FME-SoE survey started a list of courses could already be found in the Indiana web-page on Formal Methods Education Resources [9]. Anticipating the risk inherent to a world-wide survey, doomed to be incomplete and inconsistent, it was decided to restrict it to European curricula. In this way, we could learn with the exercise before embarking on such a voluminous task, which would demand more resources than those available in the subgroup.

Structure of the paper

The remainder of this paper is structured as follows. In the next section we mention some related work in the area of formal method education. Section [*] presents the FME-SoE strategy and the structure of a provisional FM body of knowledge which underlies data classification in the survey. In section [*] we proceed to a brief analysis of our data sample. The main body of the paper ends with an evaluation of the work carried out so far, which leads to plans for future work.

The remainder of the paper consists of four annexes, three listing the data which underlies the three projections discussed in section [*] and a glossary of acronyms or keywords used in the contents classification of each course or module.

Related work

There is currently a world-wide concern for «mathphobia» and the increasing loss of mathematical consistency in higher-education, the ultimate resource base of science. Among many pointers to this topic, and further to [9], we select the following two, which share our concerns concerning FM-teaching: The following workshops have addressed formal methods education:
  • Industrial Training and University Education in Formal Methods tutorial at FME'97, an earlier FME attempt to address the topic.
  • Teaching Formal Methods: Practice and Experience -- a One Day Workshop at Oxford Brookes University (12 December 2003) organised by the Applied Formal Methods Group (Oxford Brookes University) in association with BCS-FACS.


Survey Description

The WWW has been the main information source for the FME-SoE survey carried out so far. This was completed by individual contacts (mostly by email) to course lecturers and by the information provided by the people who have replied to the FME-SoE call for participation, which was put on-line as soon as the subgroup was created.

At the time of writing, FME-SoE has surveyed 117 courses spreading over 58 higher-education institutions across 13 European countries and involving (at least) 91 academic staff.

Further to objective information (course name, contact person, WWW links etc), the courses have been tagged with subjective information in the form of keywords intended for contents classification («subjective» meaning that in many cases it was not obvious what to write, often because the course contents were not readily available).

Three different kinds of keyword were found to be relevant to the survey:

  • main topics, or broad areas (38 keywords)
  • notations/languages (24 keywords), and
  • tools (39 keywords).
A glossary of all keyword acronyms can be found in appendix [*]. Pointersto WWW sites describing such acronyms have been recorded wherever available. A total number of 365 websites have been browsed and recorded in the survey at the time of writing.

As soon as the collection of main topics, notations/languages and tools was found to be minimally representative, the prospect of organizing them in an FM ontology was considered. However, ontologies are hard to build and it was soon realized that such a task would demand far more effort and team-work than initially planned. So, it was decided to organize the available data in a provisional, simple FM body of knowledge structured in five broad areas:

  • Foundations
  • Formal specification paradigms
  • Correctness, verification and calculation
  • Formal semantics
  • Support for executable specification
  • Other Topics
At a lower level of rank, fourteen sub-areas could be identified:
  • Set-theoretic/topological foundations of Formal Methods
  • Logical foundations of Formal Methods
  • Type-theoretic foundations of Formal Methods
  • Algebraic foundations of Formal Methods
  • Property oriented specification
  • Model oriented specification
  • Multi-paradigm specification
  • Correct by construction
  • Correct by verification
  • Correct by machine checking
  • Refinement techniques
  • Programming language semantics
  • Formalizing distribution, concurrency and mobility
  • Declarative programming
The table in appendix [*] frames all keywords into this two-layered hierarchical body of knowledge [*]. Wherever possible, the entries in the table refer to the SEEK units mentioned earlier on, as well as to some of the units of the CC2001 CS body of knowledge (directly or indirectly) related to formal methods.


Survey Analysis

The surveyed data have been collected (in abstract-syntax format) in a textual database which was subject to a number of simple «data-mining» operations available from a runnable functional specification of the courses database. The following main analytical projections were identified:
  • Survey of courses per topic;
  • Survey of courses per notations, notation variants or specification languages;
  • Survey of courses per tools.

The enumeration of all courses selected per each projection is given in tabular format in appendices [*], [*] and [*], respectively. The last two are ordered by number of course units selected. Column labels in tables should be read as follows:

Institution
-- Institution name (abbreviated).
Ref
-- Local identification of module in institution (if available / applicable).
Y/S
-- Year/semester of module, wherever such a time schedule is mentioned or can be safely inferred [*].
Module
-- Module name.
Contact
-- Lecturer or contact person.
Topics/Langs/Tools
-- Acronyms of module topics, (specification) languages, notations and tools. All these entries can be looked up in the glossary of appendix [*].

A brief (quantitative) analysis of these projections follows, in the form of histograms. Concerning the first projection, we have obtained the histogram of Fig. [*]which summarizes the tables of appendix [*]. It can be observed that model-oriented specification (FM06) is by far the most popular topic in the survey, followed by the teaching of concurrency (FM13) and logical foundations (FM02). A third group of topics includes model checking (cf. FM10), support for executable specification (cf. FM14) and formal semantics (FM12). Comparatively less widespread is the teaching of algebraic approaches to formal specification (topics FM04 and FM05). Last in the list is multi-paradigm specification (FM07), a topic whose relevance in industrial case-studies and scientific meetings (eg. FME symposia) is not yet mirrored in the curricula.

Another question we have tried to answer is concerned with whether courses are focussed and go deep on particular subjects, or they tend to spread over many topics in a light-weight («breadth-first») manner. Without further inspection of cross-breedings among topic areas, we found out that 47 courses focus onto one topic area only, 36 courses spread over two topic areas and 21 courses spread over three areas. All other courses remaining are even less focussed.

Figure: Number of courses per main topic area
\begin{figure}\begin{center} \begin{histogram}{110}{60}{0}{1}{2} \map{FM07}{1} \... ...FM02}{27} \map{FM13}{27} \map{FM06}{52}\end{histogram}\end{center}\end{figure}

Concerning the second projection, we have identified 24 notations (or notation variants) and/or (specification) languages, which are listed in appendix [*] ranked by the number of courses which teach or address them [*]. Altogether, we have obtained the histogram of Fig. [*]. The popularity of specification languages and methods such as Z [15] and B [1] is consistent with the widespread teaching of model-oriented specification unveiled by the previous projection. The somewhat surprising rôle of functional programming languages such as Haskell [7] and SML [5] is due to their use in animation (rapid prototyping) or to the development of libraries written in such languages which support teaching.

Figure: Number of courses per language/notation
\begin{figure}\begin{center} \begin{histogram}{50}{100}{0}{1}{4} \map{ELotos}{1}... ...7} \map{SML}{7} \map{B}{15} \map{Z}{16}\end{histogram}\end{center}\end{figure}

Concerning the third projection, and despite the fact that 65 courses don't mention any support tools in their website description, we have identified 39 tools or (formal specification) libraries, which are listed in appendix [*] ranked by the number of courses which mention them. However, the analysis of the corresponding histogram (Fig. [*]) requires some care, as it is not always obvious from websites which particular tools are being imposed or recommended. Very often, tools are not even mentioned (in particular if they are open source software) and are implicit from the context [*]. Almost half of the tools offer support for model-oriented methods such as B, Z or VDM [4]. The prominent rôle of model checking tools is to be remarked, notably SPIN [6] and UPPAAL [8].

Figure: Number of courses per tools
\begin{figure}\begin{center} \begin{histogram}{40}{170}{0}{1}{9} \map{Actress}{1... ...{UPPAAL}{5} \map{SPIN}{6} \map{VDMT}{6}\end{histogram}\end{center}\end{figure}

Conclusions and Further Work

This report presents the information gathered so far in a survey of FM-courses (on-going action of FME-SoE) in higher education institutions across Europe. Although far from being fully representative, this survey already provides a sample of the target data amenable to multi-dimensional analysis. However, it is lacking consistency in two respects:

Shortcomings of web-based survey.

A survey focussed on web-data is not enough because of the following aspects:
  • Availability: many courses are not available on-line or are password-protected (usually within campus intranets).
  • Temporal aspects: most websites are «snapshot»-like in the sense that they only show today's data. Elective courses may «exist» but be inactive in the current academic year.
  • WWW dynamics: URLs are very volatile and change all the time. Therefore, referential integrity can hardly be maintained. (Will the WWW ever be considered an information system as we understand the concept nowadays?)

Shortcomings of sampling method.

  • The FME-SoE course sample database is not yet fully representative. In particular, it is geographically asymmetric. Countries such as Spain and Germany, just to mention only two, are far from properly documented.
  • The classification of modules (keyword-based) is perhpas too simple. It can be improved once a more effective ontology or body of knowledge is developed.

Where are we?

The survey reported in this paper is not yet a fully achieved exercise. May it serve as a stimulus for course lecturers to advertise their teaching experiences and results, eventually leading to a self-updatable central repository accessible on a «wiki»-basis hosted by FME. The more representative it becomes, the more effective it will be in helping lecturers to cross-compare their teaching and newcomers to adopt particular teaching approaches or styles.

We have, nevertheless, a basis to work on. The information already available can be used to inspect each institution's thread of modules. Consistent/successful threads can eventually be selected as prototypical and proposed as (FME) recommended curricular guidelines.

Our final concern should be to equip each standard with suitable (FME recommended) teaching material (or links to such a material). Like the ACM/IEEE task force have done, we should not aim at proposing a single, standard curriculum, but rather to find our own alternatives in FM curricula. For instance, similarly to the Imperative-first, Objects-first alternatives in section 7.6 of [12], FM specialists may eventually find evidence that FM intrductory courses can be of class Light-FM-first, Set-theory-first, etc. Future collaboration with the ACM/IEEE Task Force on Computing Curricula would be very welcome and beneficial for both sides.

Need for an FM ontology

The overall success of FME-SoE will rely on reaching consensus about the FM area of research and teaching: sooner or later, some kind of FM («meta») domain analysis will be required. Ever since Carl Linnaeus times, the activity of framing a universe of discourse into classes has always been regarded as essential to the birth of effective science. Addressing this hot topic demands effective answers to questions such as
  • What is a formal method?
    Answer in the Wikipedia, the free encyclopedia: A scientific and engineering discipline of rigorous reasoning about correctness of computer programs, based on the use of symbolic logic.
    Perhaps the ultimate target of any formal method (in computing as elsewhere in engineering, as stressed by [10]) is captured by the following «stamp», which most software houses don't use at all:
    \psfig{figure=LogoCorrectInside.eps,height=20mm}
    This entails the need for languages amenable to mathematical reasoning under a careful balance between descriptive power and calculational (reasoning) power [*].

  • What is the borderline between mathematical foundations and formal methods «as such»?

  • What is the borderline between informal and formal methods? What is a «rigorous» method?

We still have a long way to go.

Bibliography

1
J.-R. Abrial.
The B-book: assigning programs to meanings.
Cambridge University Press, 1996.

2
J. Bowen.
World wide web virtual library of formal methods, 2004.
Available from http://www.afm.sbu.ac.uk.

3
J. Cuadrado.
Teach formal methods.
Byte, page 292, December 1994.

4
J. Fitzgerald and P.G. Larsen.
Modelling Systems: Practical Tools and Techniques for Software Development .
Cambridge University Press, 1st edition, 1998.

5
Michael R. Hansen and Hans Rischel.
Introduction to Programming using SML.
Addison-Wesley, 1999.
ISBN 0-201-39820-6.

6
Gerard J. Holzmann.
The Spin Model Checker: Primer and Reference Manual.
Addison-Wesley, 2003.
ISBN 0-321-22862-6, 608 pages.

7
S.L. Peyton Jones.
Haskell 98 Language and Libraries.
Cambridge University Press, Cambridge, UK, 2003.
Also published as a Special Issue of the Journal of Functional Programming, 13(1) Jan. 2003.

8
Kim G. Larsen, Paul Pettersson, and Wang Yi.
UPPAAL in a nutshell.
Int. Journal on Software Tools for Technology Transfer, 1(1-2):134-152, 1998.

9
K. Fisler (maintainer).
Formal methods education resources, 2002.
Website hosted by the Department of Computer Science, Worcester Polytechnic Institute. Available from http://www.cs.indiana.edu/formal-methods-education/.

10
D. Mandrioli.
A few preliminary thoughts about education on formal methods within (university) curricula, 2003.
Working document available from the FME-SoE website.

11
J. N. Oliveira.
«Bagatelle in C arranged for VDM SoLo».
Journal of Universal Computer Science, 7(8):754-781, 2001.
Special Issue on Formal Aspects of Software Engineering (Colloquium in Honor of Peter Lucas , Institute for Software Technology, Graz University of Technology, May 18-19, 2001).

12
The Joint ACM/IEEE-CS Task Force on Computing Curricula.
Computing curricula 2001: Computer Science -- Final Report.
Technical report, Association for Computing Machinery and IEEE Computer Society, December 2001.

13
The Joint ACM/IEEE-CS Task Force on Computing Curricula.
Computing curriculum - Software Engineering.
Technical report, Software Engineering Education Knowledge (SEEK), February 2004.
Public Draft 3.1.

14
FME Subgroup on Education.
A survey of formal methods courses in european higher education, 2004.
Web version (HTML) available from http://www.fmeurope.org/ $\mapsto$ Formal Methods $\mapsto$ Education.

15
J. M. Spivey.
The Z Notation -- A Reference Manual.
Series in Computer Science. Prentice-Hall International, 1989.
C. A. R. Hoare.


Tentative Body of Knowledge for Formal Methods

The table which follows provides a classification for all the keywords employed in the survey (see the glossary in appendix [*]). Wherever possible, the entries in the table refer to the SEEK units mentioned earlier on, as well as to some of the following units of the CC2001 CS body of knowledge (directly or indirectly) related to formal methods:
  • DS1. Functions, relations, and sets
  • DS2. Basic logic
  • DS3. Proof techniques
  • DS5. Graphs and trees
  • PF3. Fundamental data structures
  • PF4. Recursion
  • AL2. Algorithmic strategies
  • PL5. Abstraction mechanisms
  • PL7. Functional programming
  • PL9. Type systems
  • PL10. Programming language semantics
  • IS3. Knowledge representation and reasoning
  • IS5. Advanced knowledge representation and reasoning
  • SE5. Software requirements and specifications
  • SE6. Software validation
  • SE10. Formal methods [elective]

Ref. Topics CC2001 SEEK04
FOUNDATIONS
FM01 Set-theoretic/topological foundations of Formal Methods
DMat Discrete Maths (ZF set theory, functions, relations, graphs, trees etc) DS1 FND.mf.1,FND.mf.5
FixP Lattice and Fixed Point Calculus
ScTD Scott Theory of Domains
FM02 Logical foundations of Formal Methods
FOL First-order logic (proof techniques, etc) DS2, DS3 FND.mf.2, CMP.fm.8
HL Hoare Logic
LamC (Typed) Lambda Calculus
TL Temporal Logic
LTL Linear Time Temporal Logic
CTL Computation Tree Logic
TLA The Temporal Logic of Actions
FM03 Type-theoretic foundations of Formal Methods
TT Type theory and type systems PL9
PolyT Polytypism and genericity
FM04 Algebraic foundations of Formal Methods
AlS Algebraic structures, initial/final algebras FND.mf.11
MPC Mathematics of Program Construction (inc algebra, category theory)
FORMAL SPECIFICATION PARADIGMS
FM05 Property oriented specification
ADT Abstract Data Types (initial algebra specification, etc)
CASL The Common Algebraic Specification Language
FM06 Model oriented specification
ASM Abstract State Machines CMP.fm.2
FPT Formal program techniques: pre-/post-conditions, invariants, proofs, verification, etc. SE10 MAA.md.2
B B-Method CMP.fm.2
VDM Vienna Development Method CMP.fm.2
VDMSL VDM Standard Language
VPP VDM++
IVDM Irish School of VDM
RSL RAISE Specification Language
OZ Object-Z Specification Language
Z Z-Notation CMP.fm.2
Alloy Alloy
FM07 Multi-paradigm specification
MPS Integration concerns, multi-paradigm specifications
CORRECTNESS, VERIFICATION AND CALCULATION
FM08 Correct by construction
AoP Algebra of Programming, relational calculus CMP.fm.4, EVO.ac.7
FM09 Correct by verification
PV Program verification SE10 MAA.md.4
BDD Binary decision diagrams
FM10 Correct by machine checking
MC Model Checking MAA.md.4
ATP Automated Theorem Proving
TFM Testing with formal methods
FM11 Refinement techniques
ARef Algorithm refinement, loop invariants, etc CMP.fm.6, CMP.fm.7
DRef Data refinement CMP.fm.6, CMP.fm.7
RC Refinement Calculus CMP.fm.6, CMP.fm.7
RefB Refinement in B CMP.fm.6, CMP.fm.7
FORMAL SEMANTICS
FM12 Programming language semantics
AS Action Semantics
ASe Algebraic Semantics PL10
FS Denotational and Operational Semantics PL10
AbsI Abstract interpretation PL5
FM13 Formalizing distribution, concurrency and mobility
PA Process algebras
CCS Calculus of Communicating Systems
CSP Communicating Sequential Processes CMP.fm.2
PiC $\Pi$-calculus
Petri Petri Nets
FSP Finite State Processes
MSC Message Sequence Charts
LOT LOTOS
ELOT Enhanced LOTOS
Estelle Estelle
SUPPORT FOR EXECUTABLE SPECIFICATION
FM14 Declarative programming
FP Functional Programming PL7
Haskell Haskell
SML The Standard ML Programming Language
CAML The CAML Language
Prolog Prolog
OTHER TOPICS
FM15
AL Algorithms and Complexity AL2
SA Software Architecture
JML Java Modelling Language
Safety Safety Analysis Techniques


Survey of Courses per Topic

FM01 -- Set-theoretic/topological foundations of Formal Methods

 
Number of courses selected: 8  
Ref Y/S Module Institution Contact Topics/Langs/Tools
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
5/ MSc Inform. Syst. Specification and Modelling Nancy D. Méry B , DMat
G53PAL 3 Programming Algebra Nottingham R. Backhouse AoP , FixP , PolyT
DTS Domain Theory Oxford G.M. Reed PiC , ScTD
SEM M Software Engineering Mathematics Oxford A. Martin DMat , Z
TC 4 Theory of Computation Porto M. Florido DMat , FS , Haskell , LamC , Prolog , TT
Formal methods in informatics Roma A. Labella ASe , FixP , ScTD

FM02 -- Logical foundations of Formal Methods

 
Number of courses selected: 27  
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

FM03 -- Type-theoretic foundations of Formal Methods

 
Number of courses selected: 9  
Ref Y/S Module Institution Contact Topics/Langs/Tools
Program Quality Verification Bologna C. Laneve AbsI , TT , TrL
Programmation fonctionnelle et preuves Lyon Y. Bertot Coq , FP , LamC , Ocaml , TT
702752 2 Programming Logics II