ERC project "CoVeCe" by Damien Pous

image

Project

Field: Morphogenesis

Research: Coinduction for Verification and Certification

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.

Max ERC Funding

1 407 413 €

Duration

Start date: 2016-04-01, End date: 2021-03-31

ERC Starting Grants

ERC Starting Grants support promising researchers who are at the beginning of an independent research career. The creation of their own research team will be funded with the grant.

For the evaluation of the researcher profile several benchmarks according to research domain and career development are taken into account. Benchmarks include publications as main author in high-ranking international journals, (translated) monographs, patents, conference presentations or (inter)national prizes and awards.

Researcher

Damien PousDamien Pous

Research director at LIP

Damien Pous' home page

Subject(s)