FCT Relatório Científico 2008 [LABORATÓRIO
DE INTELIGÊNCIA ARTIFICIAL E CIÊNCIA DE COMPUTADORES]
|
Group Description |
|
|
Title of Research
Group: |
(RG-COMP-Norte-Porto-27-1036) |
|
Principal Investigator: |
Sabine Babette Broda |
|
Main Scientific Domain: |
Engenharia
Electrotécnica e Informática |
|
Group Host Institution: |
Universidade
do Porto |
|
Funding, source, dates |
|
|
Funding, source,
dates |
|
|
18327 FCT Plurianual 2008 32200 FCT Project RESCUE
2008 + salaries of team members,
University of Porto 2008 + grants,
FCT, Gulbenkian, others 2008 |
|
|
Objectives
& Achievements |
|
|
Objectives |
|
|
- Definition of efficient
and usable reduction strategies for the implementation of linear programming
languages; - Resource analysis (space)
for lazy functional programming languages. - Encoding of Kleene algebra
in the Coq theorem prover to produce code security certificates for being
applied in the future on a Proof-Carrying-Code platform. - To develop, in partnership
with industrial partners (EFACEC, Critical Software), a methodology for the
formal design and verification of satefty-critical systems. We plan to apply
such methodology to the formal design of Operating systems for embedded
systems (with CRITICAL SOFTWARE) and railway signaling systems (with EFACEC). - Verification of temporal
properties of safety critical systems. Coordination languages used for the
design of safety critical systems usually do not include a formal
verification stage that would give some rigorous and verifiable insurance
with respect to the temporal behavior (and complement other static safety
mechanisms). We plan to explore and define such a cooperation between model
checker and coordination languages. These activities will be
pursued in the scope of the new Computer Science Group that results from the merge
of the APS, FMC and LCC groups. |
|
|
Main Achievements |
|
|
- In the paper (S. Alves, M.
Florido, I. Mackie, F.-R. Sinot: Minimality in a Linear Calculus with
Iteration. Electr. Notes Theor. Comput. Sci. 204: 163-179 (2008)) we defined
a feasible efficient reduction strategy for linear based languages. This
strategy is optimal for a weak notion of reduction similiar to the one used
in functional programming languages. - We defined a realistic cost-aware
operational semantics for lazy functional programming languages. This is the
basis of the resource analysis we are developing now. - We have encoded regular
expressions, regular languages, Kleene algebra, Kleene algebra with tests and
the deductive rules of propositional Hoare logic as Kleene algebra with
tests' theorems. Manual verification of programs written in a toy
While-language is already achievable. - One of the first step to
the design of a DbC platform that take care of resources consumption is a
comparative study of Hoare based approach to the safety of programs. This
study was presented at CoRTA'08 and is still an ongoing work. Therefore it
will serve as a basis for the mentioned DbC platform. |
|
|
Group Productivity |
|
|
Publications in peer review
Journals |
|
|
David Pereira and Nelma Moreira, KAT and PHL in
COQ, Journal of Computer Science and Information Systems, Special Issue on
Compilers, Related Technologies and Applications. Volume 5, Number 2,
December 2008 ISSN: 1820-0214. Also in Corta'08 proceedings. Simão Melo de Sousa (Ed.): Journal of Computer
Science and Information Systems, Special Issue on Compilers, Related
Technologies and Applications. Volume 5,
Number 2, December 2008 ISSN: 1820-0214. |
|
|
Other publications
International |
|
|
Maria João Varanda, Pedro Rangel Henriques, Simão
Melo de Sousa (Eds.). Proceedings
of the conference Corta’08 "COmpilers, Related
Technologies and Applications". IPB Publisher, 2008. ISBN:
978-972-745-096-1. M. Barbosa,
T. Brouard, S. Cauchie,
S. Melo de Sousa: Secure Biometric Authentication
with Improved Accuracy. ACISP 2008: 21-36. Lecture Notes in Computer Science
5107 Springer. 2008, ISBN 978-3-540-69971-2. Sandra Alves,
Mário Florido, Ian
Mackie, François-Régis Sinot:
Minimality in a Linear Calculus with Iteration. Electr. Notes Theor. Comput. Sci. 204: 163-179 (2008). D. Pereira, E. Oliveira and
N. Moreira, Formal Modelling
of Emotions in BDI Agents, Eighth Workshop on Computational Logic in
Multi-Agent Systems (CLIMA-VIII), Porto, Portugal, Springer-Verlag, LNAI, 5056, pp. 62-81, 2008. Maria João Varanda, Pedro Rangel Henriques, Simão
Melo de Sousa (Eds.). Proceedings
of the conference Corta’08 "COmpilers, Related
Technologies and Applications". IPB Publisher, 2008. ISBN: 978-972-745-096-1. |
|
|
Other publications
National |
|
|
David Pereira, Mobile code
security based on Kleene algebras
and temporal logic, MAP-i PhD Programme,
Universities of Minho,
Aveiro and Porto, Portugal, 2008., |
|
|
Internationalization |
|
|
We have ongoing
collaborations with: - King´s College/UK (Maribel
Fernandez) - École
Polytechnique/France (Ian Mackie) - RISC/Austria (Temur Kutsia) - University of St. Andrews/Scottland (Kevin Hammond) - Laboratoire
d'Informatique de l'Université
de Tours/France (Thierry Brouard) - Institut
National de Recherche en Informatique
et Automatique/France (Gilles Barthe) - Institut
National de Recherche sur
les Transports et leur Sécurité/France
(George Mariano) - Laboratoire
d'Informatique Fondamentale
d'Orléans/France (Frédéric
Loulergue) - Laboratoire
de Recherche en Informatique,
Université de Paris-Sud/France
(Jean-Christophe Filliâtre) We also started two new colaborations with Chalmers University (Koen Claessen) and CMU (Karl Crary) - this last collaboration is in the scope of the
CMU-Portugal Research Program and includes a joint PhD supervision (Mário Florido and Karl Crary). |
|
|
Future Research |
|
|
Objectives |
|
|
The main objectives for the
following years are: - Keep the leading role in
the area of linearity in programming languages and calculi. More
specifically, we aim to apply the fundamental results obtained in the
previous years to programming languages (functional programming languages),
generalizing these results to Turing complete computation models. - Increase the research
effort in the area of analysis of resource (time, space) consumption by
computer programs. In this area we aim to give both theoretical and practical
contributions in the following topics: resource analysis for embedded
systems, type systems for controlling complexity, deductive and semantic
methods to analyze resources and practical applications of resource analysis
and design By contract based approaches to ressource
consumption analysis. - In the area involving
mobile code security based on Kleene algebra (and
extensions) and temporal logic, future work and research goals include
research on the expressivity of the previous formal methods for specifying mobile
code security properties, the development of Verification Condition Generator
for discharging proof-obligations based on these properties, and the
development of proof tactics for automating the generation of proofs for
these obligations in the Coq theorem prover. These activities will be
pursued in the scope of the new Computer Science Group that results from the
merge of the APS, FMC and LCC groups. |
|
|
Funding, source,
dates |
|
|
expected 10043 FCT Plurianual 2009, depends on outcome of pending evaluation 32200 FCT RESCUE project
2009 We applied (the decision is
not known yet) to an FCT project on Linearity in programming languages and to
an FCT/British Council cooperation project for the organization of an
International Workshop in the area, co-located with the 18th EACSL Annual
Conference on Computer Science Logic 2009. |
|