• Duration: October 2005 - October 2008
  
• Global Summary (MERIT Coordinated Project):
  In accordance with the main objectives of the Spanish I+D National Plan, the goal of this project is to contribute to the understanding of systems and tools for the rapid development of reliable software. In more general terms, the project will contribute to the application of formal or rigorous methods, especially logic-based techniques, to the real needs of programming languages and the process of software development. We will mainly focus our efforts on the need for special methodologies for the development of trusted software for mobile computing. In this context issues related to heterogeneous and distributed systems, with specific characteristics and limited resources dealing with data that is heterogeneous both in terms of content and representation, are of great interest. To satisfy this need, we propose the enriching of languages and methods of declarative (multi-paradigm) programming. This ambitious project will focus on the development of new tools, languages, and environments which will give automatic support for specification, analysis, debugging, manipulation and optimization of systems of heterogeneous software, all based upon a rigorous formal base. To accomplish this goal the research team brings with it broad experience with formal methods in the area of programming languages. The contributions of this project will mainly center around the following themes:
  • Distribution models with the implicit use of certificates which guarantee the trustworthiness of mobile code.
  • Technologies for proving complex functional properties and resource requirements through abstract interpretation.
  • Rigorous methods that permit the optimization of programs for execution on different systems with different available resources.
  • New methods that combine constraint solvers and decision procedures.
  • Formal techniques for analysis and debugging and their combination into integrated environments.
  • New frameworks for the design of domain-specific languages embedded into declarative languages.
  • The design of new languages and tools for modelling dynamic concurrent systems and for querying and manipulating semi-structured data.
  The proposed research will produce both theoretical and practical results. On the one hand, the theoretical component, coupled with the semantics of the programming languages being considered, will provide a strong formal base for the systems which will be developed. On the other hand, the practical component, essential in the field in which we work, will manifest itself in the implementation of a number of tools and environments for the construction of robust and reliable software. This project is a coordinated proposal including three different research groups spread throughout four Spanish universities along with the collaboration of seven researchers from foreign centers. All of these participants have a great deal of experience in research, development and innovation in the field of programming languages and formal methods.

Participants/Subprojects: