ADVENT

Architecture-driven verification of systems software

 Coordinatore FUNDACION IMDEA SOFTWARE 

 Organization address address: Campus de Montegancedo s/n
postcode: 28223

contact info
Titolo: Mr.
Nome: Juan José
Cognome: Collazo Nieto
Email: send email
Telefono: 34911012202
Fax: 34911011358

 Nazionalità Coordinatore Spain [ES]
 Totale costo 1˙366˙371 €
 EC contributo 1˙075˙824 €
 Programma FP7-ICT
Specific Programme "Cooperation": Information and communication technologies
 Code Call FP7-ICT-2011-C
 Funding Scheme CP
 Anno di inizio 2013
 Periodo (anno-mese-giorno) 2013-04-01   -   2016-03-31

 Partecipanti

# participant  country  role  EC contrib. [€] 
1 FUNDACION IMDEA SOFTWARE ES coordinator 0.00
2    KATHOLIEKE UNIVERSITEIT LEUVEN

 Organization address address: Oude Markt 13
city: LEUVEN
postcode: 3000

contact info
Titolo: Ms.
Nome: Sofie
Cognome: Heroes
Email: send email
Telefono: +32 16 329979
Fax: +32 16 326515

BE (LEUVEN) participant 0.00
3    MAX PLANCK GESELLSCHAFT ZUR FOERDERUNG DER WISSENSCHAFTEN E.V.

 Organization address address: Hofgartenstrasse 8
city: MUENCHEN
postcode: 80539

contact info
Titolo: Mr.
Nome: Volker Maria
Cognome: Geiss
Email: send email
Telefono: 4968190000000
Fax: 4963190000000

DE (MUENCHEN) participant 0.00
4    TEL AVIV UNIVERSITY

 Organization address address: RAMAT AVIV
city: TEL AVIV
postcode: 69978

contact info
Titolo: Ms.
Nome: Lea
Cognome: Pais
Email: send email
Telefono: +972 3 6408774
Fax: +972 3 6409697

IL (TEL AVIV) participant 0.00

Mappa


 Word cloud

Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.

world    software    nnthe    real    techniques    verification    architecture    building    reliability    tools    informally    programmers    forms   

 Obiettivo del progetto (Objective)

Systems software such as operating system kernels, hypervisors, database engines, web servers and language run-times forms the foundation of any modern computer system. It is extremely complex and hard to get right, with bugs making whole services unavailable or opening the doors of seemingly secure systems to viruses and criminals. Ensuring its reliability is thus imperative for building future trustworthy ICT infrastructures.nnThe advent project will develop innovative methods and tools for cost-effective verification of real-world systems software, making it possible to guarantee an unprecedented level of reliability. We will achieve this by exploiting a trend among programmers to use informally described patterns, idioms, abstractions and other forms of structure contained in their software, which are together called its architecture. Building on the emerging technology of separation logic, we will formalise such software engineering concepts used by systems programmers to reason about their software informally, and will use the results to drive the design of verification techniques. This is a radically novel approach to the problem of verifying complex software: it departs from the common practice of building generic verification tools that, not being able to take advantage of programmers' knowledge and intuition, do not scale to big and complicated systems.nnThe architecture-driven verification techniques resulting from the project have the potential to yield a dramatic leap in the cost-benefit ratio of the verification technology. This will allow verification to scale to systems of real-world size and complexity that so far have been beyond the reach of quality assurance methods guaranteeing correctness.

Altri progetti dello stesso programma (FP7-ICT)

TELL ME (2012)

Technology Enhanced Learning Livinglab for Manufacturing Environments

Read More  

UpScale (2014)

From Inherent Concurrency to Massive Parallelism through Type-based Optimizations

Read More  

Serenoa (2010)

Multidimensional context-aware adaptation of Service Front-ends

Read More