Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Modélisation et vérification d'algorithmes en Coq

  • Subject: [Frama-c-discuss] Modélisation et vérification d'algorithmes en Coq
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
  • Date: Tue, 02 Mar 2010 17:31:21 +0100
Dear Frama-C users,

Sorry about this message in French, but its purpose is to announce
lessons about the COQ system that will be given in French anyway.
If you don't speak French and are still interested about that,
there will be similar lessons in English in China in August.
You can also have a look at this introduction :
http://hal.inria.fr/inria-00001173

--------------------------------------------------
Ecole CEA-EDF-INRIA
"Mod?lisation et v?rification d'algorithmes en Coq : une introduction"
Paris, 7-11 juin 2010,
http://www.inria.fr/ecoles-cea-edf-inria

Le syst?me Coq fournit un langage de programmation fonctionnelle et un cadre de 
raisonnement pour effectuer des preuves sur les programmes.  Le pouvoir 
expressif du langage est suffisant pour d?crire des logiciels aussi puissants 
que des compilateurs et faire des preuves math?matiques aussi difficiles que le 
th?or?me des quatre couleurs.  Dans cette ?cole nous abordons les techniques de 
programmation et de preuve de fa?on pragmatique et progressive.  Les sujets 
abord?s sont :

- programmation r?cursive
- manipulations de listes et d'entiers
- d?monstration par r?currence
- d?finition de nouveaux types de donn?es
- programmation par filtrage et raisonnement par cas
- propri?t?s inductives
--------------------------------------------------

-- 
Anne Pacalet  : http://www-sop.inria.fr/members/Anne.Pacalet/