b2llvm: B developments onto the LLVM

LLVM-Logo-Derivative-1David Deharbe – Universidade Federal do Rio Grande do Norte, Natal, Brazil


In this talk we describe a multi-platform code generator for the B method. In particular, we present a translation procedure from a larghe subset of the B language for implementations towards LLVM source code. This translation is defined formally as a set of rules defined recursively on the abstract syntax for B implementations. It already handles most elements of the B language and is being extended to the full language. We describe different strategies to validate the generated LLVM code.