Abstract
We present b2llvm, a multi-platform code generator for the B-method. The b2llvm code generator currently handles the following elements of the B language: simple data types, imperative instructions and component compositions. In particular, this paper describes a translation for essential implementation constructs of the B language into LLVM source code, implemented into the b2llvm compiler. We use an example-based approach for this description.
V. Medeiros Jr—The research presented in this paper was partially supported by CNPq projects 308008/2012-0 and 573964/2008-4 (National Institute of Science and Technology for Software Engineer - INES).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-book: assigning programs to meanings. University Press, Cambridge (1996)
Ambert, F., Bouquet, F., Legeard, B., Peureux, F., et al.: BZ-Testing-Tools (2002)
Bodeveix, J.-P., Filali, M., Muñoz, C.: A formalization of the B-method in Coq and PVS. In: Electronic Proc. B-User Group Meeting FM 99, pp. 33–49 (1999)
Chartier, P.: Formalisation of B in Isabelle/HOL. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 66–82. Springer, Heidelberg (1998)
ClearSy. ComenC, B0 implementation translation into C language (2008). http://www.comenc.eu
ClearSy. Atelier B User Manual Version 4.0. Clearsy System Engineering (2009)
Jaeger, É., Dubois, C.: Why would you trust B? In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 288–302. Springer, Heidelberg (2007)
Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE/ACM International Symposium on Code Generation and Optimization, pp. 75–88 (2004)
Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)
Leuschel, M., Butler, M.: ProB: An automated analysis toolset for the B method. Software Tools for Technology Transfer (STTT) 10(2), 185–203 (2008)
de Matos, E.C.B., Moreira, A.M.: Beta: A B based testing approach. In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol. 7498, pp. 51–66. Springer, Heidelberg (2012)
Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: POPL, pp. 427–440 (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bonichon, R., Déharbe, D., Lecomte, T., Medeiros, V. (2015). LLVM-Based Code Generation for B. In: Braga, C., Martí-Oliet, N. (eds) Formal Methods: Foundations and Applications. SBMF 2014. Lecture Notes in Computer Science(), vol 8941. Springer, Cham. https://doi.org/10.1007/978-3-319-15075-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-15075-8_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15074-1
Online ISBN: 978-3-319-15075-8
eBook Packages: Computer ScienceComputer Science (R0)