Executing and Verifying Higher-Order Functional-Imperative Programs in Maude

Abstract : We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting language: the concrete and symbolic execution of programs; their verification with respect to properties expressed in Reachability Logic, a language-parametric generalisation of Hoare Logic; and the verification of program-equivalence properties. Our approach is proved sound and is implemented in Full Maude by taking advantage of its reflective features and module system.
Type de document :
Article dans une revue
Journal of Logical and Algebraic Methods in Programming, Elsevier, 2017, pp.45. 〈10.1016/j.jlamp.2017.09.002〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01586341
Contributeur : Pal Dream <>
Soumis le : mardi 12 septembre 2017 - 16:33:53
Dernière modification le : vendredi 22 septembre 2017 - 14:17:57

Fichier

wrla-jlamp-R2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Vlad Rusu, Andrei Arusoaie. Executing and Verifying Higher-Order Functional-Imperative Programs in Maude. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2017, pp.45. 〈10.1016/j.jlamp.2017.09.002〉. 〈hal-01586341〉

Partager

Métriques

Consultations de
la notice

37

Téléchargements du document

6