CORCON
Correctness by Construction
| Coordinatore | UNIVERSITY OF LEEDS
Organization address
address: WOODHOUSE LANE contact info |
| Nazionalità Coordinatore | United Kingdom [UK] |
| Totale costo | 285˙600 € |
| EC contributo | 285˙600 € |
| Programma | FP7-PEOPLE
Specific programme "People" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013) |
| Code Call | FP7-PEOPLE-2013-IRSES |
| Funding Scheme | MC-IRSES |
| Anno di inizio | 2014 |
| Periodo (anno-mese-giorno) | 2014-01-01 - 2017-12-31 |
Partecipanti
| # | ||||
|---|---|---|---|---|
| 1 |
UNIVERSITY OF LEEDS
Organization address
address: WOODHOUSE LANE contact info |
UK (LEEDS) | coordinator | 58˙800.00 |
| 2 |
UNIVERSITAET SIEGEN
Organization address
address: HERRENGARTEN 3 contact info |
DE (SIEGEN) | participant | 39˙900.00 |
| 3 |
UNIVERSITA DEGLI STUDI DI PADOVA
Organization address
address: VIA 8 FEBBRAIO 2 contact info |
IT (PADOVA) | participant | 37˙800.00 |
| 4 |
LUDWIG-MAXIMILIANS-UNIVERSITAET MUENCHEN
Organization address
address: GESCHWISTER SCHOLL PLATZ 1 contact info |
DE (MUENCHEN) | participant | 33˙600.00 |
| 5 |
STOCKHOLMS UNIVERSITET
Organization address
address: Universitetsvaegen 10 contact info |
SE (STOCKHOLM) | participant | 29˙400.00 |
| 6 |
SWANSEA UNIVERSITY
Organization address
address: SINGLETON PARK contact info |
UK (SWANSEA) | participant | 25˙200.00 |
| 7 |
UNIVERSITA DEGLI STUDI DELL'INSUBRIA
Organization address
address: Via Ravasi 2 contact info |
IT (VARESE) | participant | 25˙200.00 |
| 8 |
UNIVERSITA DEGLI STUDI DI GENOVA
Organization address
address: VIA BALBI 5 contact info |
IT (GENOVA) | participant | 21˙000.00 |
| 9 |
UNIVERSITY OF STRATHCLYDE
Organization address
address: Richmond Street 16 contact info |
UK (GLASGOW) | participant | 14˙700.00 |
Mappa
Word cloud
Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.
Obiettivo del progetto (Objective)
'As software becomes ever more ubiquitous in our lives, the need to ensure it runs without error becomes ever more important. Restarting a phone is a simple, if inconvenient task; restarting an aeroplane in mid-flight is not an option! Correct by construction programming offers a revolutionary approach to program verification where programs can contain not just computations as is normal, but also logical proofs of the correctness of these computations. The simple fact that such programs compile provides formal, i.e. mathematical, guarantees of the correctness of the program. In particular, there is no need for post-hoc testing of software etc.
Fundamental to the implicit marriage of computation and logic inherent within correct by construction programming is the choice of the right logical systems and concepts upon which programming languages ought to be built. This reflects the symbiotic relationship between logic, programming, and the design of programming languages—any attempt to sever this connection will diminish each component. This proposal brings together internationally leading researchers from both inside Europe and outside Europe to work on exactly what logical structures are needed for correct by construction programming and how those logical structures can then by turned into concrete programming artefacts. In order to produce fundamental work which stands the test of time, we work not with specific programming languages but with mathematical abstractions of them. The recent development of dependently typed programming languages capable of supporting correct by construction programming makes this a very timely proposal, while the billions spent on software every year makes the potential impact of this proposal very significant.'