CPROVER
Validation of Concurrent Software Across Abstraction Layers
| Coordinatore | THE CHANCELLOR, MASTERS AND SCHOLARS OF THE UNIVERSITY OF OXFORD
Spiacenti, non ci sono informazioni su questo coordinatore. Contattare Fabio per maggiori infomrazioni, grazie. |
| Nazionalità Coordinatore | United Kingdom [UK] |
| Totale costo | 1˙368˙355 € |
| EC contributo | 1˙368˙355 € |
| Programma | FP7-IDEAS-ERC
Specific programme: "Ideas" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013) |
| Code Call | ERC-2011-StG_20101014 |
| Funding Scheme | ERC-SG |
| Anno di inizio | 2011 |
| Periodo (anno-mese-giorno) | 2011-12-01 - 2016-11-30 |
Partecipanti
| # | ||||
|---|---|---|---|---|
| 1 |
THE CHANCELLOR, MASTERS AND SCHOLARS OF THE UNIVERSITY OF OXFORD
Organization address
address: University Offices, Wellington Square contact info |
UK (OXFORD) | hostInstitution | 1˙368˙355.00 |
| 2 |
THE CHANCELLOR, MASTERS AND SCHOLARS OF THE UNIVERSITY OF OXFORD
Organization address
address: University Offices, Wellington Square contact info |
UK (OXFORD) | hostInstitution | 1˙368˙355.00 |
Mappa
Word cloud
Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.
Obiettivo del progetto (Objective)
'The cost of software quality assurance (QA) dominates the cost of IT development and maintenance projects. QA is frequently on the critical path to market. Effective software QA is therefore decisive for the competitiveness of numerous industries that rely on IT, and essential for government tasks that rely heavily on IT.
This research programme will provide a pragmatic solution to the most pressing issue in software QA in mainstream software engineering: the use of concurrency. Programmers make use of numerous favors of concurrency in order to achieve better scalability, savings in power, increase reliability, and to boost performance. The need for software that makes diligent use of concurrent computational resources has been exacerbated by power-efficient multi-core CPUs, which are now widely deployed, but still unfertilized due to the lack of appropriate software. Concurrent software is particularly difficult to test, as bugs depend on particular interlavings between the sequential computations. Defects are therefore difficult to reproduce and diagnose, and often elude even very experienced programmers.
We propose to develop new, ground-braking reasoning and testing technology for this kind of software, with the goal of cutting the staff effort in QA of concurrent effort in half. We will use a tightly integrated combination of scalable and performant testing technology and Model Checking and abstract interpretation engines to prune the search. Every aspect of the research programme is geared towards improving the productivity of the average application programmer. Our theories and reasoning technology will therefore be implemented in a seamless fashion within the existing, well-accepted programming environments Visual Studio and Eclipse, in close collaboration with Microsoft and IBM.'