SLE 2026 paper:
Engineering Verified Model Transformations through a Proof-Based Language Workbench

Akram Idani, German Vega

🏆 Distinguished Artefact Award
DOI: 10.1145/3806383.3815523
Researchr: details/sle-2026/sle-2026/12/Engineering-Verified-Model-Transformations-through-a-Proof-Based-Language-Workbench
T4A: Workbenches
- BCerT is an extension of the Meeduse language workbench for verified transformation engineering.
T5D: Formal Methods
- The central contribution is formal verification of model transformations using the B method, theorem proving, and model checking.
T1C: Behavioural Semantics
- The paper uses the B method, theorem proving, and model checking to establish correctness of executable semantics.
T3B: Transformation Languages
- The paper focuses on model transformations and their specification as B operations or events.
T4C: Vertical Transformation
- The certified UML-state-machine-to-Event-B transpiler is a vertical transformation/refinement scenario.

The page is maintained by Dr. Vadim Zaytsev a.k.a. @grammarware. Last updated: July 2026.