FCT strategic project PEst-OE/EEI/UI0027/2011: 22,254€

FCT-funded projects: RESCUE 32k€, FAVAS 8K€, CANTE 4K€

QREN project: Prosinal 20K€

* Declarative Information Systems

- Anchor all developments in well-defined semantics.

- Study extended forms of pattern matching (flexible arity with context variables).

- Higher-level abstraction in the database management operations of insertion, update and delete.

- Start developing a meta system for managing COMPASS applications, using COMPASS itself.

* Linearity

( provide answers to open problems regarding linearity and linearisation in the context of programming languages )

- definition of linear systems for particular programming paradigms;

- using linearity information for the definition of efficient implementations of programming languages.

* Kolmogorov complexity

- clarify relationships with entropy measures

* Program verification

- Proof Assistants and Proof by Computer

- Proof-carrying code

* Web analysis

- apply specialized languages to the verification of Web content

RESEARCH:

An introductory book on program verification was published by Springer.

A paper on a simple denotational semantics for Cube, the base language of COMPASS, was presented at ICLP 2011, the major conference on logic programming, with a corresponding journal publication.

A recursive linear language was defined, reported in a paper in the International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), and in another paper accepted for publication in the Journal of Logic and Computation.

A (denotacional) semantic treatment of the WCET analysis in multicore environments was developed.

An article on Entropy Measures vs. Kolmogorov Complexity was published in the Entropy journal.

An implementation was made of a verifier for a a low-level assembly language (ARM) based on denotational semantics and abstract interpretation.

The language XCentric was applied to content verification in distributed collaboration scenarios.

TECHNOLOGY TRANSFER:

- The first mathematically and mechanically modeled and proved SIL4 level (highest in the CENELEC standard) signaling system in the world (using SCADE, in collaboration with EFACEC).

- Educed: Awarded (by the GSI Accelerators program) spin-off by supervised students incubated at Plug and Play Tech Center (PPTC – at Silicon Valley – USA). A method and tool support for the formal treatment of requirement analysis and automatic test generation (from natural language requirements).

HUMAN RESOURCES:

6 ongoing PhD

4 MS concluded, 1 ongoing

Sandra Alves, Maribel Fernández, Mário Florido and Ian Mackie. “An Introduction to Linearity”, Journal of Logic and Computation, to appear in 2012.

António Porto (2011): A Structured alternative to Prolog with simple compositional semantics. Theory and Practice of Logic Programming, 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue 11(4-5), pp. 611-627, doi:10.1017/S1471068411000202. ISI indexed

Andreia Teixeira, Armando Matos, André Souto, and Luís Antunes (2001). Entropy Measures vs. Kolmogorov Complexity. Entropy, Vol 13, No. 3, pp-595-611. doi:10.3390/e13030595 ISI indexed

ISI indexed:

José Carlos Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification. Series: Undergraduate Topics in Computer Science, 1st Edition, Springer, 2001. ISBN: 978-0-85729-017-5.

António Porto (2011): An Alternative High-level Approach to Interaction with Databases. In Salvador Abreu & Dietmar Seipel, editors: Applications of Declarative Programming and Knowledge Management; 18th International Conference, INAP 2009; Évora, Portugal, November 2009; Revised Selected Papers, Lecture Notes in Artificial Intelligence 6547, Springer, pp. 20-39, doi:0.1007/978-3-642-20589-7.

V. Rodrigues, S. M. Sousa, J. P. Pedroso and M. Florido: Certifying Execution Time. Foundational and Practical Aspects of Resource Analysis (FOPARA) 2011. LNCS, Springer, 2011.

V. Rodrigues, M. Florido, S. M. de Sousa. A Functional Approach to Worst-Case Execution Time Analysis. 20th Int. Workshop on Functional and (Constraint) Logic Programming, WFLP 2011, LNCS vol. 6816, Springer, 2011.

Other:

Liliana Alexandre and Jorge Coelho. Filtering XML Content for Publication and Presentation on the Web. Sixth IEEE International Conference on Digital Information Management, The University of Melbourne, Australia. IEEE 2011.

Sandra Alves, Maribel Fernández, Mário Florido and Ian Mackie. Linearity and recursion in a typed lambda-calculus. International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'11), ACM, 2011.

Sandra Alves, Maribel Fernández and Ian Mackie. A new graphical calculus of proofs. Proceedings TERMGRAPH 2011, Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 48, pag. 69-84, 2011.

C. Amaral, M. Florido and Patrik Jansson: Interfacing Dynamically Typed Languages and Why: Reasoning about Lists and Tuples. Tenth ACM SIGPLAN Erlang Workshop, ACM, 2011.

Coelho J., Florido, M. (2011). Semantic Verification in an Open Collaboration Scenario. In J. Park, T. Yang, L. Changhoon (Eds.) Future Information Technology. Communications in Computer and Information Science 185. (pp. 44-53). Springer. 978-3-642-22309-9.

Armando Matos, André Souto and Andreia Teixeira. Distinguishing probability ensembles. Computability in Europe 2011: Models of Computation in Context - Abstract and Handout Booklet, St. Kliment Ohridski University Press, 2011.

Liliana Alexandre and Jorge Coelho. XCentric-based Visual Approach to Web Content Verification. 9ª XML: Aplicações e Tecnologias Associadas, Escola Superior de Estudos Industriais e de Gestão, Vila do Conde, 1 e 2 de Julho 2011; 71-82.

André de Matos Pedro, Maria João Frade, Ana Paula Martins and Simão Melo de Sousa. Aprendizagem de processos semi-Markovianos generalizados: dos sistemas de eventos discretos estocásticos aos testes e à verificação. INForum 2011. 8-9th September 2011, Coimbra, Portugal.

Vítor Rodrigues, Mário Florido and Simão Melo de Sousa. Back Annotation in Action: from WCET Analysis to Source Code Verification. INForum 2011. 8-9th September 2011, Coimbra, Portugal.

Simão Melo de Sousa. Outils et Techniques pour la verification formelle da la plateforme Javacard. Édition Universitaires Européenes. February 2011. ISBN: 978-613-1-53931-2

6 ongoing PhD

4 MSc concluded

MSc 1 ongoing

• Cube - a structured logic programming language platform

• NACS – a natural attributive language for defining conceptual schemes

• NADI – a natural attributive query language for databases

• Compass – a compositional, modular and parametric architecture for service systems

• member of the Executive Board of the International Federation for Computational Logic (IFCoLog) (Sandra Alves)

• steering committeee, PPDP – Principles and Practice of Declarative Programming (António Porto)

• program committee, track on Coordination Models, Languages and Applications (CM) of the 26th ACM SAC conference (António Porto)

EVOLVE - Evolutionary Validation, Verification and Certification (EUREKA-ITEA2). In collaboration with Critical Software.

PROSINAL - Rigorous Design, validation and certification of railways signaling systems. QREN - In collaboration with EFACEC

STORK - Secure Identity Across Borders Linked (ICT Policy Support Programme), under the CIP (Competitiveness and Innovation Programme), and co-funded by the European Community. In collaboration with Multicert.

Visits to the group:

- Kevin Hammond, U. St.Andrews, Scotland

- Steffen Jost, U. Muenchen, Germany

Participation in external PhD committees:

- Mário Florido, Universitat Politecnica de Valencia (Daniel Romero)

Stays abroad:

- Sandra Alves, visiting Research Associate at DI, King's College of London, 1 Sep 2010 - 28 Feb 2011, collaborating with Maribel Fernández.

- Sandra Alves, visiting scientist at TYPICAL – Laboratoire d’informatique de l’Ecole Polytechnique, 28 Aug - 28 Sep 2011, collaborating with Ian Mackie.

- Simão Sousa, Invited researcher at PROVAL, INRIA Saclay-CNRS FR. March 2011.

Joint supervison of PhDs:

- Mário Florido, with Patrick Jansson (Chalmers, Sweden) and Temur Kutsia (RISC, Austria).

RESCUE - REliable and Safe Code execUtion for Embedded systems. FCT-PTDC/EIA/65862/2006. (headed by Simão Melo de Sousa) January 2008 - March 2011. Partners: LIACC/DCC/FCUP, DIUM,DMUM, ISEP, UBI

FAVAS - A FormAl Verification PlAtform for real-time Systems. FCT-PTDC/EIA-CCO/105034/2008 (2010-2012). The FAVAS project aims at developing mathematically well-founded and pratically usegul technology to formally verify real-time systems such as avionic controllers. Coordination of the Work Package on source code and contract based methods. Partners: UBI/LIACC, MITI/UMa, CCTC/DIUM

Cante - Descriptional and computational complexity of formal language FCT-PTDC/EIA-CCO/101904/2008 (2010-2012) . (LIACC member) - LIACC/DCC/FCUP