Skip to Main content Skip to Navigation
Journal articles

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.
Complete list of metadata

Cited literature [44 references]  Display  Hide  Download

https://hal.inria.fr/hal-01586341
Contributor : Pal Dream <>
Submitted on : Tuesday, September 12, 2017 - 4:33:53 PM
Last modification on : Friday, September 29, 2017 - 9:41:31 PM
Long-term archiving on: : Wednesday, December 13, 2017 - 2:00:01 PM

File

wrla-jlamp-R2.pdf
Files produced by the author(s)

Identifiers

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, vol. 93, pp.68-91. ⟨10.1016/j.jlamp.2017.09.002⟩. ⟨hal-01586341⟩

Share

Metrics

Record views

328

Files downloads

1418