Génération de programmes efficaces et vérifiés

La majorité des langages utilisés dans l'industrie sont impératifs et permettent l'utilisation de pointeurs. Pourtant, la certification de ce type de programmes est encore difficile et mal maitrisée, entraînant souvent la mise en place de limitations des possibilités du langage. Elle s'effectue ensuite, pour la vérification à l'aide d'assistants de preuve, par transformation du code en un langage logique ou fonctionnel vérifiable.

La méthode présentée ici emprunte le chemin inverse, et permet de générer du code impératif avec pointeurs à partir de code fonctionnel vérifiable. La difficulté est alors de pouvoir générer du code efficace, c'est à dire utilisant à bon escient des pointeurs et des variables muables.
 

Online Copy

Available as PDF
 

BibTeX Entry

(preliminary)

@InProceedings{ GiMaSt2009.1,
author = {Giorgino, Mathieu and Matthes, Ralph and Strecker, Martin},
title = "{Génération de programmes efficaces et vérifiés}",
booktitle = "{Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Toulouse, 26/01/09-28/01/09}",
year = {2009},
to_appear = {à paraître},
publisher = {},
pages = {},
language = {français},
note = {}
}