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

Christiano Braga; Narciso Mart\'i-Oliet

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

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2108.07878 v1 pith:NA6KF3B7 submitted 2021-08-17 cs.SE cs.LO

Christiano Braga , Narciso Martí-Oliet This is my paper

classification cs.SEcs.LO

keywords maudeabstractdescriptionsenvironmentexecutablemachinenotationsemantics

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

abstract

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 $\pi$ 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.

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB
cs.LO 2026-07 conditional novelty 6.0 of 10

An interactive sequent prover for Event-B was built by encoding over 600 proof rules in Prolog inside ProB.

Pith tools