FOVEDIS SIGNED
Formal specification and verification of distributed data structures
Total Cost €
0EC-Contrib. €
0Partnership
0Views
0FOVEDIS project word cloud
Explore the words cloud of the FOVEDIS project. It provides you a very rough idea of what is the project "FOVEDIS" about.
Project "FOVEDIS" data sheet
The following table provides information about the project.
| Coordinator |
UNIVERSITE PARIS DIDEROT - PARIS 7
There are not information about this coordinator. Please contact Fabio for more information, thanks. |
| Coordinator Country | France [FR] |
| Total cost | 1˙300˙000 € |
| EC max contribution | 1˙300˙000 € (100%) |
| Programme |
1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC)) |
| Code Call | ERC-2015-STG |
| Funding Scheme | ERC-STG |
| Starting year | 2016 |
| Duration (year-month-day) | from 2016-05-01 to 2021-04-30 |
Partnership
Take a look of project's partnership.
| # | ||||
|---|---|---|---|---|
| 1 | UNIVERSITE DE PARIS | FR (PARIS) | coordinator | 1˙300˙000.00 |
| 2 | UNIVERSITE PARIS DIDEROT - PARIS 7 | FR (PARIS) | coordinator | 0.00 |
Map
Project objective
The future of the computing technology relies on fast access, transformation, and exchange of data across large-scale networks such as the Internet. The design of software systems that support high-frequency parallel accesses to high-quantity data is a fundamental challenge. As more scalable alternatives to traditional relational databases, distributed data structures (DDSs) are at the basis of a wide range of automated services, for now, and for the foreseeable future.
This proposal aims to improve our understanding of the theoretical foundations of DDSs. The design and the usage of DDSs are based on new principles, for which we currently lack rigorous engineering methodologies. Specifically, we lack design procedures based on precise specifications, and automated reasoning techniques for enhancing the reliability of the engineering process.
The targeted breakthrough of this proposal is developing automated formal methods for rigorous engineering of DDSs. A first objective is to define coherent formal specifications that provide precise requirements at design time and explicit guarantees during their usage. Then, we will investigate practical programming principles, compatible with these specifications, for building applications that use DDSs. Finally, we will develop efficient automated reasoning techniques for debugging or validating DDS implementations against their specifications. The principles underlying automated reasoning are also important for identifying best practices in the design of these complex systems to increase confidence in their correctness. The developed methodologies based on formal specifications will thus benefit both the conception and automated validation of DDS implementations and the applications that use them.
Publications
| year | authors and title | journal | last update |
|---|---|---|---|
| 2017 |
Constantin Enea, Ondřej Lengál, Mihaela Sighireanu, Tomáš Vojnar Compositional entailment checking for a fragment of separation logic published pages: 575-607, ISSN: 0925-9856, DOI: 10.1007/s10703-017-0289-4 |
Formal Methods in System Design 51/3 | 2020-04-06 |
| 2017 |
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil Proving Linearizability Using Forward Simulations published pages: 542-563, ISSN: , DOI: 10.1007/978-3-319-63390-9_28 |
Computer Aided Verification - 29th International Conference, {CAV} 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II} 2017 | 2020-04-06 |
| 2017 |
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency published pages: 170-200, ISSN: , DOI: 10.1007/978-3-662-54434-1_7 |
Programming Languages and Systems - 26th European Symposium on Programming, {ESOP} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings 2017 | 2020-04-06 |
| 2017 |
Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri Abstract Semantic Diffing of Evolving Concurrent Programs published pages: 46-65, ISSN: , DOI: 10.1007/978-3-319-66706-5_3 |
Static Analysis - 24th International Symposium, {SAS} 2017, New York, NY, USA, August 30 - September 1, 2017, Proceedings 2017 | 2020-04-06 |
| 2017 |
Ahmed Bouajjani, Constantin Enea, Chao Wang Checking Linearizability of Concurrent Priority Queues published pages: 16:1--16:16, ISSN: , DOI: 10.4230/LIPIcs.CONCUR.2017.16 |
28th International Conference on Concurrency Theory, {CONCUR} 2017, September 5-8, 2017, Berlin, Germany 2017 | 2020-04-06 |
| 2017 |
Constantin Enea, Ondřej Lengál, Mihaela Sighireanu, Tomáš Vojnar {SPEN:} {A} Solver for Separation Logic published pages: 302-309, ISSN: , DOI: 10.1007/978-3-319-57288-8_22 |
{NASA} Formal Methods - 9th International Symposium, {NFM} 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings 2017 | 2020-04-06 |
| 2017 |
Michael Emmi, Constantin Enea Sound, complete, and tractable linearizability monitoring for concurrent collections published pages: 1-27, ISSN: 2475-1421, DOI: 10.1145/3158113 |
Proceedings of the ACM on Programming Languages 2/POPL | 2020-04-06 |
Are you the coordinator (or a participant) of this project? Plaese send me more information about the "FOVEDIS" project.
For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.
Send me an email (fabio@fabiodisconzi.com) and I put them in your project's page as son as possible.
Thanks. And then put a link of this page into your project's website.
The information about "FOVEDIS" are provided by the European Opendata Portal: CORDIS opendata.