b2llvm: B developments onto the LLVM

David Deharbe – Universidade Federal do Rio Grande do Norte, Natal, Brazil

Abstract:

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.

http://www.ic.ufal.br/evento/cbsoft2014/en/keynotes-sbmf.html