The following table provides information about the project.
CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE CNRS
There are not information about this coordinator. Please contact Fabio for more information, thanks.
|Coordinator Country||France [FR]|
|Total cost||1˙407˙413 €|
|EC max contribution||1˙407˙413 € (100%)|
1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
|Duration (year-month-day)||from 2016-04-01 to 2021-03-31|
Take a look of project's partnership.
|1||CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE CNRS||FR (PARIS)||hostInstitution||1˙407˙413.00|
Software and hardware bugs cost hundreds of millions of euros every year to companies and administrations. Formal methods like verification provide automatic means of finding some of these bugs. Certification, using proof assistants like Coq or Isabelle/HOL, make it possible to guarantee the absence of bugs (up to a certain point).
These two kinds of tools are crucial in order to design safer programs and machines. Unfortunately, state-of-the art tools are not yet satisfactory. Verification tools often face state-explosion problems and require more efficient algorithms; certification tools need more automation: they currently require too much time and expertise, even for basic tasks that could be handled easily through verification.
In recent work with Bonchi, we have shown that an extremely simple idea from concurrency theory could give rise to algorithms that are often exponentially faster than the algorithms currently used in verification tools.
My claim is that this idea could scale to richer models, revolutionising existing verification tools and providing algorithms for problems whose decidability is still open.
Moreover, the expected simplicity of those algorithms will make it possible to implement them inside certification tools such as Coq, to provide powerful automation techniques based on verification techniques. In the end, we will thus provide efficient and certified verification tools going beyond the state-of-the-art, but also the ability to use such tools inside the Coq proof assistant, to alleviate the cost of certification tasks.
Work performed, outcomes and results: advancements report(s)
Are you the coordinator (or a participant) of this project? Plaese send me more information about the "COVECE" 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 (firstname.lastname@example.org) 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 "COVECE" are provided by the European Opendata Portal: CORDIS opendata.
Photon High Way - Integrated single-photon sources: crossing the chasmRead More
Property and Democratic Citizenship: The Impact of Moral Assumptions, Policy Regulations, and Market Mechanisms on Experiences of EvictionRead More
Popular Sovereignty vs. the Rule of Law? Defining the Limits of Direct DemocracyRead More