Hola,
¿eres nuevo aquí?

Regístrate gratis y conecta tu empresa con financiación pública, partners y proyectos.

Tengo cuenta

Regístrate

Ver video

VSSC

Financiado

Cerrado

Verifying and Synthesizing Software Compositions

One of the first things a programmer must commit to in developing any significant piece of software is the representation of the data. In applications where performance or memory consumption is important, this representation is of... ver más

31/03/2018

TAU

2M€

Presupuesto del proyecto: 2M€

Líder del proyecto

TEL AVIV UNIVERSITY No se ha especificado una descripción o un objeto social para esta compañía.

TRL 4-5

Fecha límite participación Sin fecha límite de participación.

Ver 2 Participantes

Financiación concedida El organismo FP7 notifico la concesión del proyecto el día 2018-03-31 No tenemos la información de la convocatoria

0% 100% 100%

Información adicional privada

No hay información privada compartida para este proyecto. Habla con el coordinador.

2 Participantes

TAU

0.00€ | Lider

ALU-FR

N.D. | Participante

Conecta tu I+D

¿Tienes un proyecto y buscas un partner? Gracias a nuestro motor inteligente podemos recomendarte los mejores socios y ponerte en contacto con ellos. Te lo explicamos en este video

Proyectos interesantes

RYC2018-025200-I Compile-time code analysis and optimization 309K€ Cerrado

PLATFORM PRACTICAL LIGHT TYPES FOR RESOURCE CONSUMPTION 219K€ Cerrado

FAULTLOCALIZATION Using Hardware Performance Counters for Functional Correctne... 75K€ Cerrado

SPADE Sophisticated Program Analysis Declaratively 1M€ Cerrado

PINDESYM Program Intelligence, Declaratively and Symbolically 2M€ Cerrado

PID2019-105455GB-C32 PRUEBAS DE SOFTWARE MAS ALLA DE LAS UNITARIAS Y DE SQL 121K€ Cerrado

Líder del proyecto

TEL AVIV UNIVERSITY No se ha especificado una descripción o un objeto social para esta compañía.

TRL 4-5

Presupuesto del proyecto 2M€

Fecha límite de participación Sin fecha límite de participación.

Descripción del proyecto One of the first things a programmer must commit to in developing any significant piece of software is the representation of the data. In applications where performance or memory consumption is important, this representation is often quite complex: the data may be indexed in multiple ways and use a variety of concrete, interlinked data structures. The current situation, in which programmers either directly write these data structures themselves or use a standard data structure library, leads to two problems: 1:The particular choice of data representation is based on an expectation of what the most common workloads will be; that is, the programmer has already made cost-benefit trade-offs based on the expected distribution of operations the program will perform on these data structures. 2: It is difficult for the programmer to check or even express the high-level consistency properties of complex structures, especially when these structures are shared. This also makes software verification in existing programming languages very hard. We will investigate specification languages for describing and reasoning program data at a much higher level. The hope is that this can reduce the inherited complexity of reasoning about programs. In tandem, we will check if the high level specifications can be semi-automatically mapped specifications to efficient data representations. A novel aspect of our approach allows the user to define global invariants and a restricted set of high level operations, and only then to synthesize a representation that both adheres to the invariants and is highly specialized to exactly the set of operations the user requires. In contrast, the classical approach in databases is to assume nothing about the queries that must be answered; the representation must support all possible operations.

Conecta tu I+D

Entra hoy

¿Olvidé mi contraseña?

Financiación

Empresas

CTIs/Universidades

Proyectos

Investigadores