Language-Independent Program Verification Using Symbolic Execution

Andrei Arusoaie 1 Dorel Lucanu 2 Vlad Rusu 3
3 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Université de Lille, Sciences et Technologies, Inria Lille - Nord Europe, CNRS - Centre National de la Recherche Scientifique
Résumé : Nous présentons une méthode automatique pour vérifier des programmes, qui ne dépend pas du langage de programmation dans lequel les programmes à vérifier sont écrits. Pour cela nous nous appuyons sur la Reachability Logic, un formalisme de spécification introduit récemment, qui peut être vu comme une alternative à la logique de Hoare, mais qui, contrairement à cette dernière, ne dépend pas du langage de programmation utilisé. La Reachability Logic est munie d'un système déductif correct et relativement complet, qui laisse beaucoup de liberté à l'utilisateur sur la manière d'appliquer les règles de déduction, mais qui n'offre pas de stratégie pour construire automatiquement des preuves. Par conséquent nous proposons ici une procédure de construction des preuves, dans laquelle l'exécution symbolique joue un rôle essentiel. Nous montrons que, moyennant des conditions raisonnables sur la sémantique des langages de programmation et sur les propriétés des programmes, notre procédure est partiellement correcte. Ceci dit en substance que, lorsqu'elle termine, la procédure résout correctement le problème de vérification de programmes à base de Reachability Logic. La terminaison ne peut être garantie car la vérification de programmes est indécidable, mais la procédure termine lorsque les propriétés contiennent suffisamment d'information pour être prouvées de manière circulaire, en s'utilisant mutuellement comme hypothèses. Nous présentons une implémentation prototype d'un outil de vérification basé sur ces idées, que nous avons implémenté dans la K framework et que nous illustrons sur des exemples de programmes non triviaux, écrits dans des langages formellement définis en K.
Type de document :
Rapport
[Research Report] RR-8369, Inria. 2014, pp.28
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00864341
Contributeur : Mister Dart <>
Soumis le : vendredi 10 octobre 2014 - 08:18:00
Dernière modification le : jeudi 11 janvier 2018 - 06:25:37
Document(s) archivé(s) le : vendredi 14 avril 2017 - 13:39:53

Fichier

jfla2015-techreport.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00864341, version 6

Citation

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu. Language-Independent Program Verification Using Symbolic Execution. [Research Report] RR-8369, Inria. 2014, pp.28. 〈hal-00864341v6〉

Partager

Métriques

Consultations de la notice

270

Téléchargements de fichiers

122