Program Equivalence by Circular Reasoning

Dorel Lucanu 1 Vlad Rusu 2
2 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
Abstract : We propose a logic and a deductive system for stating and automatically proving the equivalence of programs in deterministic languages having a rewriting-based operational semantics. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the program-equivalence problem as we state it. We show that our approach is suitable for proving the equivalence of both terminating and non-terminating programs, and also the equivalence of both concrete and symbolic programs. The latter are programs in which some statements or expressions are symbolic variables. By proving the equivalence between symbolic programs, one proves in one shot the equivalence of (possibly, infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. We also report on a prototype implementation of the proposed deductive system in the K Framework.
Type de document :
Communication dans un congrès
Integrated Formal Methods, Jun 2013, Turku, Finland. Springer, LNCS 7940, pp.362-377, 2013, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00820871
Contributeur : Mister Dart <>
Soumis le : lundi 6 mai 2013 - 18:31:18
Dernière modification le : jeudi 11 janvier 2018 - 06:25:37
Document(s) archivé(s) le : mardi 4 avril 2017 - 05:48:36

Fichier

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

Identifiants

  • HAL Id : hal-00820871, version 1

Collections

Citation

Dorel Lucanu, Vlad Rusu. Program Equivalence by Circular Reasoning. Integrated Formal Methods, Jun 2013, Turku, Finland. Springer, LNCS 7940, pp.362-377, 2013, Lecture Notes in Computer Science. 〈hal-00820871〉

Partager

Métriques

Consultations de la notice

404

Téléchargements de fichiers

285