# B Maude: A formal executable environment for Abstract Machine Notation Descriptions

arXiv: https://arxiv.org/abs/2108.07878 · HTML: https://mlsanity.com/paper/2108.07878/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Aug 2021.

## Built on by (most cited first, 1 of 1)

- [Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB](https://mlsanity.com/paper/2607.21191/) (2026)

## Abstract (arXiv)

We propose B Maude, a prototype executable environment for the Abstract Machine Notation implemented in the Maude language. B Maude is formally defined and results from the implementation of the semantics of AMN as denotations in the π Framework, a realization of Mosses' Component-based Semantics and Plotkin's Interpreting Automata. B Maude endows the B method with execution by rewriting, symbolic search with narrowing and Linear Temporal Logic model checking of AMN descriptions.