The main source of funding for the research of our group is the Plurianual Program from FCT: 48,170 €

Funding from FCT Project RESCUE: 32,200 €

+ salaries of team members from U. Porto, U. Beira Interior, I. Polytechnic Porto

+ grants FCT, Gulbenkian, others

The integration of António Porto in the group brought a renewed interest in information systems, with the approach of fully basing their construction

on declarative programming techniques. We believe this is a promising and viable road towards the general LIACC aims of software and information

processing reliability. More specifically, we target the design and construction of high-level tools for the development of information systems that

integrate conceptual modelling, service-oriented architecture, declarative programming, and dynamic contextual composition, to attain high

effectiveness in the deployment, maintenance and evolution of applications. For 2009 the main objectives were the consolidation of a suitable logic

programming platform and of components for high-level interaction with relational databases.

Below are the objectives related to continuation of previous work:

* Geometric problems

- To study coverage and visibility problems, as well as the side-trip location problem for GPS-related applications.

* Linearization

- To study extensions of the linear lambda-calculus with both a restricted iterator and recursion, to overcome the very weak expressive power.

* Types

- To extend regular types with sequences and to study some algebraic properties of this new type language, aiming to solve some problems in the

composition of different specifications for semi-structured data.

* Regular Languages

- To study relationships between the descriptional complexities of automata and of the corresponding measures for regular expressions.

- To develop average-case analysis of algorithms for regular languages equivalence and conversions between equivalent regular languages

representations.

* Software verification

- To explore a formal approach based on Kleene Algebra.

- To study enhancements and applications of the semi-formal testing methodology.

* Software tools

- Development of high-performance symbolic manipulation software environments for formal languages.

- Development of XML based tools for the edition, annotation, classification and search of multimedia documents.

* The DIVERT traffic simulator (http://divert.ncc.up.pt), developed mainly by Luís Damas, definitely continued to contribute to the visibility of LIACC

during 2009, raising great interest from academia and industry. A new layer for 3D-simulation of driving situations is under development in the scope

of the DRIVE-IN project (CMU-PT/NGN/0052/2008, http://drive-in.cmuportugal.org). The use of DIVERT for other applications has also been addressed,

e.g. in virtual traffic lights systems and in testing an industrial traffic control system (GERTRUDE, France) employing real or simulated traffic

data. Several links with industry were set up (GERTRUDE, NDRIVE, GeoLink).

* The continued study of an extension of the linear lambda-calculus using a closed reduction strategy showed a huge increase in expressive power over

previous linear versions of Gödel's System T, which are closed at construction rather than at reduction. We showed that a linear T with closed

reduction is as powerful as T (article accepted for publication in TCS).

* Design and implementation of Cube, a robust logic programming platform with structural principles and powerful libraries. The novelties include

structured alternatives to Prolog's cut, contextual use of assignments, tuple-valued parameters, and very flexible value display controlled by style

and mode using inheritance with overriding.

* Design and implementation (in Cube) of a high-level approach to database interaction, with a conceptual modelling language NACS and a natural query

language NADI influenced by natural language noun phrases, with the power to properly handle temporal and multi-lingual data.

* Work on Computational Geometry, aiming at an efficient implementation of buffer and window queries for use in GPSMan, led to an algorithm for finding

points near a polyline, and to the development of a library for Voronoi/Delaunay planar decompositions.

* Relationship established between two methods for testing regular language equivalence: an algebraic method for regular expressions (re) and the

Hopcroft and Karp (1971) method for deterministic finite automata (dfa) (and its extension to non deterministic finite automata (nfa)). Experimental

results show that these methods are faster then the ones that rely on dfa minimization.

* New improvements for GPSMan, including support for pre- or user-defined plug-ins, with a new release (6.4.1) made public in December.

* An interactive graphical interface for automata visualization and manipulation.

* Formalization in the COQ theorem prover of an algorithm for testing the equivalence of regular expressions.

* Implementation of a new approach to build XML schemas in a collaborative way, based on computing intersection between sequences of regular types.

* An XML based editor for the classification of documents that allows the definition of category hierarchies.

* Comparison made between re measures and equivalent nfa sizes, based on experimental results.

Marco Almeida, Nelma Moreira, and Rogério Reis. Antimirov and Mosses's rewrite system revisited. International Journal of Foundations of Computer Science, 20(4):669{684, Aug 2009.

Luís Antunes, Armando Matos, André Souto, and Paul Vitanyi. Depth as randomness deficiency. Theory of Computing Systems, 45(4):724{739, Nov 2009.

Nelma Moreira and Rogério Reis. Series-parallel automata and short regular expressions. Fundamenta Informaticae, 91(3-4):611-629, 2009.

Alexandre Pinto, André Souto, Armando Matos, and Luís Antunes. Commitment and authentication systems. Designs Codes and Cryptography, 53(3):175-193, Dec 2009.

André Almeida, Marco Almeida, José Alves, Nelma Moreira, and Rogério Reis. FAdo and GUItar: Tools for automata manipulation and visualization. In S. Maneth, editor, CIAA 2009: Fourteenth International Conference on Implementation and Application of Automata, volume 5642 of LNCS, pages 65-74. Springer, 2009.

Marco Almeida, Nelma Moreira, and Rogério Reis. Testing equivalence of regular languages. In Workshop on Descriptional Complexity of Formal Systems (DCFS09), Magdeburg, Germany, July 2009. Also in Electronic Proceedings in Theoretical Computer Science.

Jorge Coelho, Mário Florido, and Temur Kutsia. Collaborative schema construction using regular sequence types. In K. Zhang and R. Ajhajj, editors, Proceedings of the 2009 IEEE International Conference on Information Reuse and Integration, pages 290-295, IEEE, 2009.

Michel Ferreira, Hugo Conceição, Ricardo Fernandes, and Rogério Reis. Locating cars through a vision enabled VANET. In 2009 IEEE Intelligent Vehicles Symposium, Vols. 1 and 2, pages 99-104, IEEE, 2009.

AntónioPorto. High-level interaction with relational databases in logic programming. In Andy Gill and Terrance Swift, editors, Practical Aspects of Declarative Languages; 11th International Symposium, PADL 2009; Savannah, GA, USA, January 2009; Proceedings, volume 5418 of Lecture Notes in Computer Science, pages 152-167. Springer, 2009.

António Porto and Francisco J. López-Fraguas (Editors). PPDP'09, Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, ACM Press, 2009.

Marco Almeida, Nelma Moreira, Rogério Reis. Testing the Equivalence of Regular Languages. Technical Report DCC-2009-01, DCC - FC & LIACC,

Universidade do Porto, 03/2009.

Joel Silva Carvalho and Simão Melo de Sousa. Verificação de Modelos em Programas HTL. In INFORUM 2009 Proceedings. FCUL, University of Lisbon, September 2009.

António Machiavelo, Rogério Reis. O Problema do Totobola. 39-45. In Boletim da SPM, 2009.

António Machiavelo, Rogério Reis. Um manuscrito perdido do Dr. Watson: Sherlock Holmes e o Sudoku Parte II, 47-65. In Boletim da SPM, 2009.

Nelma Moreira, David Pereira e Simão Sousa. On the mechanization of Kleene algebra in Coq. Technical Report DCC-2009-03, DCC - FC & LIACC, Universidade do Porto, 04/2009.

Ph.D.

----

Stéphane Cauchie. From pattern recognition to the security for biometry. UBI / Univ. Tours.

------

Master

---

Ivone Amorim. Criptografia com curvas elípticas. FCUP.

José António Borges. Crivo Quadrático. FCUP.

Joel Carvalho. Verificação Automatizada de Sistemas de Tempo Real Críticos. UBI.

Bruno Caxeira. Infrastrutura de chaves públicas. FCUP.

Henrique Costa. Desenvolvimento formal de um sistema de sinalização ferroviária de acordo com o normativo CENELEC usando o SCADE. UBI.

André Pasos. Towards a formally designed and verified embedded operating system: case study using the B Method. UBI.

Manuel Preliteiro. Contribution to Governemental e-ID platforms, The Portuguese and the Eurpoean Citizen Cards. UBI.

Alexandra Queirós. Votações Electrónicas e a Cifra de Paillier. FCUP.

DIVERT traffic simulator: Development of Inter-VEhicular Reliable Telematics, 2007-2009. http://divert.ncc.up.pt/, http://drive-in.cmuportugal.org.

GPSMan version 6.4.1: a graphical manager of GPS (Global Positioning System) data, 1998-2009, distributed and used world-wide. http://www.ncc.up.pt/gpsman

Cube: a robust logic programming system with structural principles and powerful libraries.

NACS and NADI: conceptual scheme compiler and query language for high-level, natural language-inspired, interaction with relational databases.

quadedge: a Tcl/Tk implementation of Voronoi/Delaunay decompositions.

FAdo: software library for automata and regular expressions manipulation.

GUItar: graphical interface for automata visualization and manipulation.

Klass: an XML based editor for the classification of documents that allows the definition of category hierarchies.

KACoq: formalization of Kleene algebra in the Coq theorem prover.

Sabine Broda and Mário Florido - members, Organizing Committee of the 18th EACSL Annual Conference on Computer Science Logic (CSL 2009).

Mário Florido - co-chair, First International Workshop on Linearity (LINEARITY 2009).

António Porto - chair (and PC member), Ana Paula Tomás - local chair, PPDP'09, the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming.

António Porto - referee, Special Track on Coordination Models, Languages and Applications (CM) at the ACM SAC 2009 (Symposium on Applied Computing).

Address recognition project with Imometrica. QREN 2009-2010. 60K€.

PROSINAL - Rigorous Design, validation and certification of railways signaling systems. QREN. In collaboration with EFACEC. 2009-2010. 39 K€.

Leader: Simão Sousa (UBI / LIACC).

António Porto - member, Editorial Board of J.UCS, the Journal of Universal Computer Science (Springer).

M. Filgueiras - member, international Scientific Board of the ESFRI Project CLARIN.

António Porto - member, Steering Committee of PPDP, the ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming.

Luís Damas - team member, project DRIVE-IN (Distributed Routing and Infotainment through Vehicular Inter-Networking, funded by FCT under CMU-Portugal program, CMU-PT/NGN/0052/2008, http://drive-in.cmuportugal.org).

Ana Paula Tomás - team member, CRUP Spanish-Portuguese Bilateral Action "Approximate Resolution of Geometric Optimization Problems".

GPSMan, developed by M. Filgueiras, is distributed and used world-wide with several collaborators abroad.

Collaborations:

* École Polytechnique, Paris (Ian Mackie)

* King´s College, London (Maribel Fernández)

* RISC Institue, Austria (Temur Kutsia)

* St. Andrews University, Scotland (Kevin Hammond)

* University of Manitoba, Winipeg, Canada (Michel Domaratzki)

* University of Western Ontario, London, Canada (Sheng Yu)

* University of Prince Edwards Island, Charlotetown, Canada (Cezar Campeanu)

DRIVE-IN - Distributed Routing and Infotainment through Vehicular Inter-Networking. CMU-PT/NGN/0052/2008.

RESCUE - REliable and Safe Code execUtion for Embedded systems. FCT- PTDC/EIA/65862/2006 (2008-2010). 161 K€ global.

FUTURE OBJECTIVES OF ONGOING RESEARCH:

* Traffic and transportation systems

- To develop a distributed version of the Divert platform for traffic simulation.

- To use Divert in projects with real-world impact.

* Geometric problems

- Continuation of the work (side-trip location, coverage, visibility), with applications to spatial database systems.

* Descriptional complexity of regular languages

- To obtain canonical forms for classes of nondeterministic finite automata (nfa) and a uniformly random generator for some nfas.

- In order to obtain small regular expressiosn (re) from automata, to characterize properties of automata underlying graphs and to define sets of

graph transformations based on algebraic re equivalences.

- Average-case analysis of algorithms for converting between regular expressions and finite automata.

* High-performance symbolic manipulation software

- To continue the development of tools for automata manipulation, for easy prototyping of new algorithms and testing performance.

- To design and implement tools for automatic drawing of automata diagrams.

* Formal verification based on Kleene Algebra (KA)

- To define and extending the Coq formalization of KA equivalence to KA extensions such as KAT, Modal KA and Timed KA.

* Linearity

- To study of the interaction between linearity and recursion in functional languages, aiming to obtain Turing complete extensions of linear

languages.

* Semi-formal testing methodology

- To enhance the automation of software testing, addressing the concrete needs of industrial partners.

* Types

- Automatic resource analysis for lazy functional programs. The goal is to define and implement an automatic type-based analysis of resource usage

for lazy functional programs. We will use an amortised analysis approach, which has previously been restricted to eager languages. From an operational

semantics for lazy evaluation we want to derive a cost model in terms of heap allocations, to prove its soundness and to provide a number of examples

demonstrating the power of our analysis.

- Extentions of type-based specification languages for the proof of functional programs to deal with concurrency and real-time control systems

programming. We propose to define a logical interpretation of annotated programs as a partial proof of its specification based on a static analysis of

the effects of the program.

- Applications of the Formula-Tree proof method in the area of type-inhabitation, now combined with analytic combinatorics, in order to obtain

asymptotic results for the average case.

--------------------

NEW RESEARCH TOPICS:

* Declarative information systems

- We want to design, implement and support COMPASS, an open source platform for building information systems along declarative principles. The

purpose is to provide a tool capable of substantially reducing the cost of setting up, maintaining and modifying sophisticated information systems.

Many novel techniques for generic programming are demanded, centered around dynamic contextual composition along hierarchies of service themes related

to the conceptual model. The grand challenge is to build change-awareness in the architecture itself, given that conceptual change is the most daunting

task facing developers of real-world applications.

* Cryptology and security of protocols

- Public-key cryptosystems based on number-theory concepts tend to be computationally expensive. On the other hand, finite automata based public-key

cryptosystems (FPAKS) exhibit good performance and its keys are relatively small. We intend to study the feasibility of this approach by defining

adequate measures and to study the security properties of the FPAKS based on those measures.

* Logic-based formal verification for Python

- Translation of an anotated subset of Python to the HL language used by the verification conditions generator WHY.

* Model checking for real-time systems based on ADA

- Development of an automatic translator able to abstract ADA tasks coordination and provide a model for which temporal properties can be analysed,

by means of a model checker.

* Rewriting

- We want to integrate rewriting with built-in unification and matching algorithms (for example sequence, context and higher-order unification). With

this, new calculi will result that we hope are models of new expressive and higer-lever declarative programming languages based on rewriting. This is a

medium and long term objective.

Project: CANTE:Descriptional and Computational Complexity of Formal Languages

Funding entity: FCT (contract PTDC/EIA-CCO/101904/2008)

Total award amount: 90,000 euros

Award period: May/2010 to May/2013

Coordinator: Rogério Reis

Project: CSI:Cryptographic Security of Individual Instances

Funding entity: FCT (contract PTDC/EIA-CCO/099951/2008)

Total award amount: 144,000 euros

Award period: March/2010 to May/2013

Coordinator: Luís Filipe Coelho Antunes (IT); at LIACC: Rogério Reis