Opendata, web and dolomites


Coinduction for Verification and Certification

Total Cost €


EC-Contrib. €






Project "CoVeCe" data sheet

The following table provides information about the project.


Organization address
address: RUE MICHEL ANGE 3
city: PARIS
postcode: 75794

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 Coordinator Country France [FR]
 Project website
 Total cost 1˙407˙413 €
 EC max contribution 1˙407˙413 € (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-04-01   to  2021-03-31


Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 


 Project objective

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.


year authors and title journal last update
List of publications.
2017 Basold, Henning; Pous, Damien; Rot, Jurriaan
Monoidal Company for Accessible Functors *
published pages: , ISSN: , DOI: 10.4230/LIPIcs.CALCO.2017.5
7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017) 2019-07-08
2017 Das, Anupam; Pous, Damien
A cut-free cyclic proof system for Kleene algebra
published pages: , ISSN: , DOI: 10.1007/978-3-319-66902-1_16
26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017) 2019-07-08
2017 Brunet, Paul; Pous, Damien
Petri Automata
published pages: , ISSN: 1860-5974, DOI: 10.23638/LMCS-13(3:33)2017
Logical Methods in Computer Science 2019-07-08
2017 Pous, Damien; Rot, Jurriaan
Companions, Codensity and Causality
published pages: , ISSN: , DOI: 10.1007/978-3-662-54458-7_7
20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017) 2019-07-08
2016 Brunet, Paul; Pous, Damien
A formal exploration of Nominal Kleene Algebra
published pages: , ISSN: , DOI: 10.4230/LIPIcs.MFCS.2016.22
41st International Symposium on Mathematical Foundations of Computer Science (MFCS) 2019-07-08
2017 Cosme-Llópez, Enric; Pous, Damien
K4-free Graphs as a Free Algebra
published pages: , ISSN: , DOI: 10.4230/LIPIcs.MFCS.2017.76
42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017) 2019-07-08
2016 Pous, Damien
Automata for relation algebra and formal proofs
published pages: , ISSN: , DOI:
HdR thesis, ENS Lyon, 2016 2019-07-08
2016 Paul Brunet, Damien Pous, Insa Stucke
Cardinalities of Finite Relations in Coq
published pages: 466-474, ISSN: , DOI: 10.1007/978-3-319-43144-4_29
7th international conference on Interactive Theorem Proving (ITP) 2019-07-08
2017 Filippo Bonchi, Daniela PetriÅŸan, Damien Pous, Jurriaan Rot
A general account of coinduction up-to
published pages: 127-190, ISSN: 0001-5903, DOI: 10.1007/s00236-016-0271-4
Acta Informatica 54/2 2019-07-08
2017 Brunet, Paul; Pous, Damien; Struth, Georg
On Decidability of Concurrent Kleene Algebra
published pages: , ISSN: , DOI: 10.4230/LIPIcs.CONCUR.2017.24
28th International Conference on Concurrency Theory (CONCUR 2017) 2019-07-08
2018 Anupam Das, Amina Doumane, Damien Pous
Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
published pages: 271-251, ISSN: , DOI: 10.29007/hzq3
EPiC Series in Computing volume 57 2019-08-05
2019 Kuperberg, Denis; Pinault, Laureline; Pous, Damien
Coinductive algorithms for Büchi automata
published pages: , ISSN: , DOI:
Developments in Language Theory 2019-08-05
2018 Bagnol , Marc; Kuperberg , Denis
Büchi Good-for-Games Automata Are Efficiently Recognizable
published pages: , ISSN: , DOI: 10.4230/LIPIcs.FSTTCS.2018.16
FSTTCS 2019-08-05
2019 Filippo Bonchi, Ana Sokolova, Valeria Vignudelli
The Theory of Traces for Systems with Probability and Nondeterminism
published pages: , ISSN: , DOI:
Logic in Computer Science 2019-08-05
2018 Damien Pous
On the Positive Calculus of Relations with Transitive Closure
published pages: , ISSN: , DOI: 10.4230/lipics.stacs.2018.3
STACS 2019-08-05
2018 Das , Anupam; Pous , Damien
Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)
published pages: , ISSN: , DOI: 10.4230/LIPIcs.CSL.2018.18
Computer Science Logic 2019-05-27
2017 Durier, Adrien; Hirschkoff, Daniel; Sangiorgi, Davide
Divergence and unique solution of equations
published pages: , ISSN: , DOI: 10.4230/LIPIcs.CONCUR.2017.7
28th International Conference on Concurrency Theory - CONCUR 2017 2019-04-18
2018 Christian Doczkal ; Damien Pous
Treewidth-Two Graphs as a Free Algebra
published pages: , ISSN: , DOI: 10.4230/LIPIcs.MFCS.2018.60
Mathematical Foundations of Computer Science (MFCS) 2019-04-18
2018 Christian Doczkal, Guillaume Combette, Damien Pous
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
published pages: 178-195, ISSN: , DOI: 10.1007/978-3-319-94821-8_11
International Conference on Interactive Theorem Proving (ITP) 2019-04-18
2018 Doumane , Amina; Pous , Damien
Completeness for Identity-free Kleene Lattices
published pages: , ISSN: , DOI: 10.4230/LIPIcs.CONCUR.2018.18
The 29th International Conference on Concurrency Theory (CONCUR) 2019-04-18
2018 Christian Doczkal, Gert Smolka
Regular Language Representations in the Constructive Type Theory of Coq
published pages: 521-553, ISSN: 0168-7433, DOI: 10.1007/s10817-018-9460-x
Journal of Automated Reasoning 61/1-4 2019-04-18

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 ( 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.

More projects from the same programme (H2020-EU.1.1.)


Economic Fluctuations, Productivity Growth and Stabilization Policies: A Keynesian Growth Perspective

Read More  

Photopharm (2020)

Photopharmacology: From Academia toward the Clinic.

Read More  


The Mass Politics of Disintegration

Read More