Funds available in 2010:

FCT plurianual funding: 30K€.

FCT-funded projects: RESCUE 32k€, FAVAS 8K€, CANTE 8K€, ASA 6K€, CSI 5K€.

QREN project: Prosinal 20K€.

* Declarative Information Systems

- Ever-higher abstraction, expressiveness and conciseness in conceptual queries.

- Automated high-level management of database tables.

- Compilation of a full service map from compositional modular descriptions.

* Descriptional Complexity of Regular Languages

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

- Average-case analysis of algorithms for regular languages equivalence and conversions between equivalent regular languages representations.

* High-performance software environments for formal languages

- 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

- Define and extend the Coq formalization of Kleene Algebra (KA) equivalence to KA extensions such as KAT, Modal KA and Timed KA.

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

* Model checking

- 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.

* Geometric problems

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

* Kolmogorov complexity

- Continue the individual characterization of cryptographic primitives using Kolmogorov complexity.

- Relate entropy measures with Kolmogorov complexity.

- Study the communication complexity of 'random functions'.

- Study the decidability of the problem: equivalence of SRL programs.

* Linearity:

- Definition of a linear language with full recursion, a relevant step in the application of linearisation to standard programming languages.

- Linearisation of other (besides functional) declarative programming paradigms such as rewriting and logic programming.

* Proofs and Types:

- Definition of a type system based on amortized analysis for resource analysis (heap usage) for a lazy functional programming language.

- Definition of a type system for a language based on rewriting with using sequence, context and higher-order variables on patterns. This new type system may have applications in program verification when querying semi-structured data is a key issue, such as XML processing, program transformation and bioinformatics;

- Investigating reduction strategies for the lambda-calculus by placing conditions on the usual beta rule. This provides a framework that can be instantiated to a number of interesting cases. The study will begin with the notion of typed reduction, in which reduction can only take place if some typing constraint is verified on the redex, irrespective of whether the whole term is typable or not.

- Defining a simple graphical representation for proofs of intuitionistic logic, inspired by both proof nets and interaction nets (two formalisms originating in linear logic), which inherits good features from each, but is not constrained by them. By the Curry-Howard isomorphism, such representation can be applied to the lambda calculus, which offers an alternative diagrammatic representation of functional computations.

* Security

- Proving and certifying security properties of real-time programs.

- Pursuing our goal of high-level database interaction, we defined relational attributes and quantification in conceptual query constraints, and provided a full treatment of manifold attributes for temporal and multi-lingual data.

- As part of the COMPASS architecture we implemented a service map compiler for information systems, from declarative theme/sub-channel modules organized in packages under topics, with computation of relevant parametric ranges for instance validation and choice menus.

- Average-size of Partial Derivative automata based on analytic combinatorial methods.

- An incremental minimization algorithm for deterministic finite automata that runs in time O(n^2).

- New heuristics methods for the conversion of FAs into equivalent small REs based on automata graph properties.

- Enhanced the interactive automata visualization tool, GUItar, with several automatic drawing graph algorithms and sophisticated interaction with external diagram formats and automata manipulation tools.

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

- Static type inference for a subset of Python.

- In the context of ADA/SPARK programs, a general transformation model to timed finite state machines was defined and prototyped. This gave rise to a tool able to model-check ADA/SPARK source programs against timing properties.

- In the context of a Proof Carrying Code based architecture, the fundamental study of a methodology for the proof, the certificate generation and the validation of timing behavior of mobile programs was conducted. This encompassed the definition of abstract interpretation based static analysis and its application to the computation of WCET bound of assembly programs. A proof of concept of an abstraction carrying code platform was designed and prototyped.

- In the scope of the work on geometric algorithms aimed at an efficient implementation of buffer and window queries for use in GPS applications, further development of our library for Voronoi/Delaunay planar decompositions made it suitable for use with hierarchical decompositions.

- Research on guarding problems on rectilinear polygons led to a polynomial time algorithm for solving the minimum vertex guard problem on the class of THIN grid orthogonal polygons. This algorithm is based on the deconstruction of the given THIN instance and exploits a tailored version of our enumeration algorithm for generic grid orthogonal polygons. Based on the generic enumeration algorithm, we also obtained an exact recursive definition of the subclass of spirals.

- Work on minimal guarding rectangular partitions (i.e., floorplans), whose complexity is still an open problem, led to the design and implementation of an algorithm for the generation of regular floorplans with a given number of rooms and without collinear edges. This class of floorplans is combinatorially complete for the guarding problem. The generation procedure is based on the existence of an Abe ordering for every floorplan and provides a direct enumeration method for this class.

- Definition of a polymorphic type system of an extension of the linear-lambda calculus with iterators, obtaining a new, efficient way of having polymorphism in iterators.

- We extended previous work on query languages for XML based on sequence unification with context unification and second-order unification, and applied this new framework to XML processing and Web reasoning.

Sandra Alves, Maribel Fernández, Mário Florido, Ian Mackie. Gödel's system T revisited. Theoretical Computer Science 411(11-13): 1484-1500, Elsevier, 2010. (ISI) (IF:1.103)

Marco Almeida, Nelma Moreira, and Rogério Reis. Testing equivalence of regular languages. Journal of Automata, Languages and Combinatorics, 2010. Accepted for publication.

Sandra Alves, Maribel Fernández, Mário Florido and Ian Mackie. Linearity and Iterator Types for Gödel's System T. International Journal on Higher-Order and Symbolic Computation, Springer. To appear, 2010.

André Carvalho, Joel Carvalho, Jorge Sousa Pinto, Simão Melo de Sousa. Model-Checking Temporal Properties of Real-Time HTL Programs. Proceedings of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'2010) 18-20 October 2010 - Amirandes, Heraclion, Crete. Lecture Notes in Computer Science, Springer, 2010.

Andreia Teixeira, André Souto, Armando Matos, Luís Antunes. Entropy Measures vs. Algorithmic Information. 2010 IEEE International Symposium on Information Theory, pages 1413-1417, IEEE Press, 2010. (ISI)

Armando Matos, André Souto and Andreia Teixeira. The largest monochromatic combinatorial rectangles with applications to Communication Complexity. Proceedings of Computers in Europe, Azores, 2010.

D. Fialho, N. Gaspar, J.S. Pinto, R. Reis and S. Melo de Sousa. Worst-Case Execution Time: From predictions to certificates. Proceedings of the Days in Logic'2010, Porto, Portugal, January 2010.

Diogo Fialho, Nuno Gaspar, Simão Melo de Sousa, Rogério Reis, and Jorge Sousa Pinto. Towards a worst-case execution time calculation platform with certificate production. In Proceedings of the 8th European Dependable Computing Conference, Valencia, Spain, April 2010.

Hugo Gouveia, Nelma Moreira, and Rogério Reis. Small nfas from regular expressions: some experimental results. In Fernando Ferreira, Hélia

Guerra, Elvira Mayordomo, and João Rasga, editors, Proceedings of 6th Conference on Computability in Europe (CIE 2010), pages 194-203, Ponta Delgada, Azores, Portugal, June/July 2010.

Jorge Coelho, Besik Dundua, Mário Florido and Temur Kutsia. A Rule-Based Approach to XML Processing and Web Reasoning. Web reasoning and Rule Systems (RR 2010). Lecture Notes in Computer Science, Springer, 2010. (ISI)

José Bacelar Almeida, Nelma Moreira, David Pereira, and Simão Melo de Sousa. Partial derivative automata formalized in Coq. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA 2010), Lecture Notes in Computer Science, Springer, 2010.

Luís Antunes, Armando Matos, Alexandre Pinto, André Souto, Andreia Teixeira. One-way functions using Kolmogorov complexity. Proceedings of Computability in Europe, Azores 2010.

Luís Antunes, Armando Matos, André Souto and Andreia Teixeira. Kolmogorov Complexity and Entropy Measures. Proceedings of Current Trends in Theory and Practice of Computer Science, 36th Int. Conf., Czech Republic, 2010.

Luís Nogueira, Luís Miguel Pinho and Jorge Coelho. Flexible and Dynamic Replication Control for Interdependent Distributed Real-Time Embedded Systems. DIPES/BICC 2010, IFIP AICT 329, pp. 63-74, Springer 2010.

Marco Almeida, Nelma Moreira, and Rogério Reis. Incremental dfa minimisation. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA 2010), volume 6482 of Lecture Notes on Computer Science, pages 39-48, Springer 2010.

N. Moreira, D. Pereira and S. Melo de Sousa. Deciding regular expressions equivalence in Coq. Proceedings of the Days in Logic'2010, Porto, Portugal, January 2010.

Nelma Moreira, Davide Nabais, and Rogério Reis. State elimination ordering strategies: some experimental results. In I. MacQuillan, G. Pighizzini, and B. Trost, editors, Proc. of 11th Workshop on Descriptional Complexity of Formal Systems (DCFS10), pages 169-180, Saskatoon, Saskatchewan, Canada, August 2010.

Paul Crocker, Vasco Nicolau, Simão Melo de Sousa. Sniffing with the Portuguese Identity Card, for fun and profit. Proceedings of ECIW'2010, Thessaloniki, Greece, July 2010. (ISI)

Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. On the average number of states of partial derivative automata. In Yuan Gao, Hanlin Lu, Shinnosuke Seki, and Sheng Yu, editors, Developments in Language Theory, 14th International Conference (DLT 2010) Proceedings, volume 6224 of Lecture Notes in Computer Science, pages 112-123, Springer 2010. DOI: 10.1007/978-3-642-14455-4_12 (ISI)

V. Rodrigues, M. Florido and S. Melo de Sousa. Pragmatic Program Transformation and Verification: an Abstract Interpretation Perspective. Proceedings of the Days in Logic'2010, Porto, Portugal, 2010.

André Almeida, Nelma Moreira, and Rogério Reis. GUItar and FAgoo: Graphical interface for automata visualization, editing, and interaction. In Luís S. Barbosa and Miguel P. Correia, editors, Inforum, Simpósio de Informática, pages 317-328, Braga, 2010.

António Machiavelo and Rogério Reis. Ainda o totobola: o singular caso dos 5. Boletim da Sociedade Portuguesa de Matemática, 2010.

Eva Maia, Nelma Moreira, and Rogério Reis. Inferência de tipos em Python. In Luís S. Barbosa and Miguel P. Correia, editors, Inforum, Simpósio de Informática, pages 515-518, Braga, 2010.

Joaquim Tojal, Carlos Carloto, José Faria and Simão Melo de Sousa. Towards a Formally Verified Kernel Module. Actas do II Simpósio de Informática, INForum'2010, Universidade do Minho, Braga, 2010.

José Alves, Nelma Moreira, and Rogério Reis. XML description for automata manipulations. In Alberto Simões, Daniela Cruz, and José Carlos Ramalho, editors, Actas XATA 2010, XML: aplicações e tecnologias associadas, pages 77-88, ESEIG, Vila do Conde, 2010.

Nuno Gaspar, Rogério Reis and Simão Melo de Sousa. Timing Analysis - From Predictions to Certificates (nominated for the best student paper award). Actas do II Simpósio de Informática, INForum'2010, Universidade do Minho, Braga, 2010.

Paul Crocker, Vasco Nicolau, Simão Melo de Sousa. A nova dimensão da entidade electrónica em Portugal. Congresso Nacional de Segurança e Defesa, Lisboa, 2010.

PhD:

Marco Almeida, "Equivalence of regular languages: an algorithmic

approach and complexity analysis", FCUP 2010.

MSc:

André Almeida, "Towards Automata Diagram Drawings", FCUP 2010.

Carlos Cardoso, "Towards a Formally verified MicroKernel using the Frama-C ToolSet", UBI 2010.

Eva Maia, "Inferência de tipos em Python", FCUP 2010.

Joaquim Tojal, "Towards a Formally verified MicroKernel using the VCC Verifier",UBI 2010.

José Alves, "An Interactive System for Automata Manipulations", FCUP 2010.

Martinho Rodrigues, "Utilização de Dispositivos Criptográficos Portáteis em Sistemas de Votação Electrónica", UBI 2010.

Nuno Gaspar, "Timing Analysis - From Predictions to Certificates", UBI 2010.

COMPASS: Concept-Oriented, Modular and Parametric Architecture for Service Systems.

FAdo: software library for automata and regular expression manipulation.

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

GUItar: graphical interface for automata visualization and manipulation.

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

A tool for model-checking ADA/SPark source programs against timing properties.

Steering Committee member:

António Porto - ACM SIGPLAN International Symposium on Principles and Practice of

Declarative Programming (2010, 2011)

Program Committee member:

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

Simão Sousa, Simpósio de Informática - INForum 2010.

Simão Sousa, Model Driven Approaches in System Development (MDASD'10) at ADBIS 2010 - Advances in Databases and Information.

Sandra Alves - Executive Board member, International Federation for Computational Logic (IFCoLog).

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

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

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

Mário Florido - reviewer of research projects submitted to the French National Research Agency (ANR).

Collaborations:

* École Polytechnique, Paris (Ian Mackie)

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

* Ludwig-Maximilians-Universität München (Steffen Jost)

* RISC Institute, Austria (Temur Kutsia)

* St. Andrews University, Scotland (Kevin Hammond)

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

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

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

* Università degli Studi di Milano (Giovanni Pighizzini)

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

ASA - Automata, Semigroups and Application. PTDC/MAT/65481/2006. 52K€ global.

CANTE - Descriptional and computational complexity of formal languages. PTDC/EIA-CCO/101904/2008. 90K€ global.

CSI - Cryptographic Security of Individual

Instances. PTDC/EIA-CCO/099951/2008. 144K€ global.

FAVAS - A FormAl Verification PlAtform for real-time Systems. PTDC/EIA-CCO/105034/2008 (2009-1012). 33K€ local.

Prosinal - certification of railroad signaling system. QREN (2010-2011). 39K€ local.

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