Skip to Main content Skip to Navigation
New interface
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
Contributor : Pal Dream Connect in order to contact the contributor
Submitted on : Tuesday, September 12, 2017 - 4:33:53 PM
Last modification on : Friday, July 8, 2022 - 10:06:44 AM
Long-term archiving on: : Wednesday, December 13, 2017 - 2:00:01 PM


Files produced by the author(s)



Vlad Rusu, Andrei Arusoaie. Executing and Verifying Higher-Order Functional-Imperative Programs in Maude. Journal of Logical and Algebraic Methods in Programming, 2017, vol. 93, pp.68-91. ⟨10.1016/j.jlamp.2017.09.002⟩. ⟨hal-01586341⟩



Record views


Files downloads