Perle de preuve: les tableaux creux

• mémoire - matière potentielle : et de permissions d' accès
• mémoire

Perle de preuve: les tableaux creux Romain Bardou* , Claude Marché** * Lab. de Recherche en Informatique, Univ Paris-Sud, CNRS, Orsay, F-91405 ** INRIA Saclay - Île-de-France, 4 rue Jacques Monod, Orsay, F-91893 Résumé. La preuve formelle de propriétés du comportement fonctionnel des programmes im- pératifs est difficile car le partage de références peut invalider de manière inattendue des inva- riants de données.

• approche capucine en bref
• capucine
• réduit aux constructions essentielles pour l'ap- proche
• langage de capucine
• tableaux creux
• régions mémoire
• preuve formelle de propriétés du comportement fonctionnel des programmes im- pératifs
• preuves
• preuve
• programmes
• programme