CerCo
# CerCo

CerCo est un compilateur pour le langage de programmation C à préservation de complexité concrète formellement certifiée. Il est maintenu et développé conjointement par les équipes de l'Université de $Bologne^,,$ l'Université Paris $Diderot^,^,^,$ et de l'Université d'Édimbourg dans le cadre du septième programme-cadre européen $(FP7)^,.$

## Intérêt de la certification de complexité

Les définitions de modèles de coûts sont prises en compte pour les langages sources et cibles ainsi que pour l'assistant de preuve tout au long de la compilation. Le compilateur retourne alors une information formellement certifiée sur la complexité du programme source.

Cela permet ainsi aux développeurs de développer une infrastructure d'assertion de temps sur le code compilé à partir du simple code source.

