|
Descripción
|
|
|---|---|
| The relevance of software grows each day, partially due to the fact that it is embedded in an ever-increasing number of devices, often controlling safety-critical applications. Therefore, it is crucial to have the means for developing, in a simple way, software which is both reliable and efficient. The overall aim of this project is to devise the required methods and tools for enabling the development of verifiable and efficient software. Programming language technology has received considerable attention in the last few decades, with important advances in language design, verification, transformation,etc., as well as in emerging techniques such as the use of proof-carrying code. An essential enabling technology for these advances is static analysis, often formalized in terms of abstract interpretation, a semantics-based approach which allows inferring a wide range of properties about program behavior which are applicable to ensuring both software correctness and efficiency, and in a way that is at the same time rigorous and highly practical. These properties include for example safe approximations of the use of different resources such as time complexity or memory usage. The level of maturity of abstract interpretation allows it to be applied to realistic programs, as proposed in this project. Another important motivation behind this proposal on the efficiency side is parallelism. With the advent of the end of Moore's Law, multi-core architectures are now mainstream, with an expected continuous increase in the number of parallel processing units in the coming years: Chip manufacturers are turning to multi-core processor designs rather than scalar-oriented frequency increases in order to improve performance. Automatically (and reliably) exploiting these parallelism capabilities in an efficient manner is an important and inevitable challenge today. It turns out that the analysis techniques and the properties to be inferred used by parallelizing compilers are the same or closely related to those mentioned above. This project brings together researchers from UPM and UCM (as well as a number of key foreign researchers) with wide expertise in the areas of static analysis, program verification, and automatic parallelization. The project focuses on developing fundamental technologies, which make them widely applicable to different programming languages and paradigms. More concretely, the researchers plan to work both on (i) their own development environment, Ciao, in order to maximize scientific progress; Ciao is used because the clean semantics of declarative programming allows concentrating on the really important aspects of the problems at hand, and (ii) Java bytecode, in order to maximize the impact of the tools and techniques developed, since Java bytecode plays nowadays a crucial role in many applications, including mobile code. | |
|
Internacional
|
No |
|
Tipo de proyecto
|
Proyectos y convenios en convocatorias públicas competitivas |
|
Entidad financiadora
|
2008-05624/TIN |
|
Nacionalidad Entidad
|
ESPAÑA |
|
Tamaño de la entidad
|
Pequeña Empresa (11-50) |
|
Fecha concesión
|
|