Programming Language Aggregation with Applications in Equivalence Checking

Résumé : Nous montrons qu'à partir des sémantiques opérationnelles de deux langages de programmation L et R il est possible de construire leur agrégation, qui est un langage dont les programmes sont des paires de programmes de L et de R. Dans ce nouveau langage, les données ou expressions communes à L et R sont factorisés afin d'éviter d'en garder deux copies distinctes. Ceci est rendu possible grâce au théorème de "pushout" qui construit un modèle de l'agrégation à partir de modèles des composantes L et R. Nous appliquons ces résultats à la preuve d'équivalence de programmes.
Type de document :
Communication dans un congrès
Third International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS 2014), Jul 2014, Vienne, Austria. 2014
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00998930
Contributeur : Mister Dart <>
Soumis le : mardi 3 juin 2014 - 08:59:23
Dernière modification le : jeudi 11 janvier 2018 - 06:25:37
Document(s) archivé(s) le : mercredi 3 septembre 2014 - 11:00:37

Fichier

pas2014_submission_14_1_.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00998930, version 1

Collections

Citation

Ştefan Ciobâcǎ, Dorel Lucanu, Vlad Rusu, Grigore Rosu. Programming Language Aggregation with Applications in Equivalence Checking. Third International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS 2014), Jul 2014, Vienne, Austria. 2014. 〈hal-00998930〉

Partager

Métriques

Consultations de la notice

258

Téléchargements de fichiers

185