|
 
|
[Urb10] Preuve automatique : techniques, outils et certification
Mémoire de HDR : Soutenue le: 29 November 2010, pp. 77, pp.: Rapporteur 1: Nachum DershowitzRapporteur 2: Jürgen Giesl
Rapporteur 3: Jean Goubault-Larrecq
Membre du jury: Claude Marché
Membre du jury: Jean-François Monin
Membre du jury: Brigitte Rozoy, : Preuve automatique : techniques, outils et certification,
Mots clés: Automated deduction, certification, formal proof, termination
Résumé:
Mes thèmes de recherche visent au développement de programmes sûrs. Ils concernent la preuve automatique ; en particulier les moyens d’apporter autant d’automatisation que possible à la vérification mécanique de propriétés des programmes.
Le contexte général de mes contributions suit un parcours commençant par les choix d’un formalisme de base et d’une propriété particulière. Il aborde pour cette dernière le développement de techniques de preuves qui doivent pouvoir être automatisées, qui s’adaptent à la pratique du développement logiciel, et dont l’efficacité va davantage se concentrer sur les problèmes rencontrés en pratique, plutôt que sur des cas pathologiques.
L’étape suivante consiste à se rapprocher des langages de programmation courants, principalement en ajoutant au formalisme de base des constructions de plus en plus expressives et en y étudiant l’extension de nos techniques automatisées : présence de symboles associatifs et commutatifs, stratégies d’évaluation, conditions, etc.
Je crois fermement que, tout au long de ce parcours, les résultats obtenus doivent être implantés : ils sont en premier lieu recherchés pour être utilisés dans des situations concrètes de développement. Les outils logiciels forment ainsi une composante essentielle de mes travaux. Se pose alors la question fondamentale de la confiance portée à ces outils, prouveurs automatiques, tout particulièrement dans
le cadre de leurs liens avec des assistants à la preuve (où les preuves sont en général développées de façon interactive, puis vérifiées mécaniquement). Tenter d’y répondre va requérir des avancées dans différents domaines : modèles formels, communication entre outils, techniques pour la preuve formelle, etc. Ces étapes franchies, on pourra commencer à envisager dans le cadre de développements formels une délégation des preuves à des outils automatiques
Commentaires:
Université Paris-Sud XI, centre d'Orsay, France
Equipe:
sys
BibTeX
| @misc { | |||
| Urb10, | |||
| title | = | "{Preuve automatique : techniques, outils et certification}", | |
| author | = | "X. Urbain", | |
| year | = | 2010, | |
| pages | = | "77", | |
| address | = | "{CEDRIC Laboratory, Paris, France}", | |
| note | = | "{Post-Doctoral Degree (Phd students supervisor) Université Paris-Sud XI, centre d'Orsay, France Rapporteur 1: Nachum Dershowitz Rapporteur 2: Jürgen Giesl Rapporteur 3: Jean Goubault-Larrecq Membre du jury: Claude Marché Membre du jury: Jean-François Monin Membre du jury: Brigitte Rozoy}", | |
| } |
