 |
UM Formal Methods Group
|
|
[ DI/UM ]
|
|---|
Interest in Formal Methods
at the Informatics Department
of Minho University
started in 1984.
By 1989 a group was set up by a protocol with the INESC
R&D institute
(see INESC Group #2361
).
Its main target was to promote the adoption of Formal Methods by industrial
partners in R&D contracts (see the CAMILA
project).
By 1997 the group stopped its formal liaison with INESC
due to
financial difficulties.
It is currently a small but active academic group mainly devoted to
program calculation and the development of the SETS
calculus for
data refinement.
Current members:
- J.N. Oliveira
(Group leader, Ph.D., Prof. Ass.)
- currently interested in SETS
-based point-free calculation
and formal calculation of distributed applications.
- L.S. Barbosa
(M.Sc., Lecturer)
- currently finishing his Ph.D. on a co-algebraic approach to
agent-refinement and calculation.
- C.J. Rodrigues
(M.Sc., Lecturer)
- currently doing a Ph.D. on relating SETS
to other reification
calculi.
- F.L. Neves
(Lic., research assistant)
- currently finishing an M.Sc. project on a SETS
animator using
genetic-algorithms to support term-rewriting.
- L.G. Ferreira
- currently doing an M.Sc. project on a SETS
-semantics for OLAP
technology.
- F.A. Silva
- currently doing an M.Sc. project on formalizing the
software component technology available in the WINDOWS environmemt.
- M.R. Henriques
- just started an M.Sc. project on formalizing a GIS domain-specific
language.
- B.C. Cortes
(final year student)
- he is finishing his workstudy in industry within the KARMA
research project. He has defined the KARMA
standard for
metadata and is relating it to UML
.
- J.C. Silva
(final year student)
- he is doing his workstudy in industry in formal reverse engineering
in the KARMA
research project. His component infers the
VDM-SL
specification of an arbitrarily large
relational database.
- R. Picas
- he is doing research on the sampling theory behind the KARMA
research project.
Past postgraduate students:
- C.G.Ferreira
- she did an M.Sc. project on a SETS
-based
``classify-by-data'' theory.
- A. Gulamhussen
- in her M.Sc. she developed a graphical editor for the
CAMILA
-workbench based on an analogy between hardware ICs
and software.
- I.S. Jourdan
- she did an M.Sc. project on the foundations of SETS
.
- R.C. Oliveira
- he studied the application of SETS
to reasoning about
subtypes and subclasses in object-oriented programming.
- M.L. Teixeira
- she formally specified and prototyped mOBJ, a subset of OBJ2.
Current areas of interest are
- formal specification and program calculi
- process refinement
- industrial application of Formal Methods
- rapid prototyping from formal specifications
- functional programming
(The URLs mentioned below are available in Portuguese.)
- Functional programming (2nd year courses 701055
and 531316
)
- Process calculi (3rd year course MP-IV
)
- Formal methods I (4th year courses 5307P2
and 7007N2
)
- Formal methods II (4th year courses 7008N2
and 5308P3
)
- Laboratory for formal methods (5th year course LMF
)
- Software development from formal specifications
(M.Sc. course EDFS
)
A sample of past or on-going R&D projects follows (in alphabetic order):
- CAMILA
(past)
- LOGCOMP
(ongoing)
- INTERLAB (past) -- a laboratory for the specification and development of
human-computer interaction layers,
partnership with Departamento de Informática
, funded by JNICT
Contract 164/90
- KARMA
(started 1998)
-- an AdI
-funded industrial contract signed with
NOVABASE Porto,
NOVABASE Lisbon and SIDEREUS
,
aiming at addressing Data Quality from novel perspectives.
These include the use of formal methods and the adoption of formal
techniques for data representation and (reverse) calculation.
- SETS
(ongoing)
- SOUR
(past)
- Temporal NBDC (past) -- an industrial contract signed with SONAE (1996)
on the design of systematic strategy for temporalizing the company's
central database system.
See the following URLs: SETS
, CAMILA
and INESC Group #2361
.
7/6/1999
Jose Nuno Oliveira
