Skip to Main content Skip to Navigation
Conference papers

Component Reuse in B Using ACL2

Abstract : We present a new methodology that permits to reuse an existing hardware component that has not been developed within the B framework while maintaining a correct design flow. It consists of writing a specification of the component in B and proving that the VHDL description of the component implements the specification using the ACL2 system. This paper focuses on the translation of the B specification into ACL2.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Yann Zimmermann <>
Submitted on : Wednesday, November 16, 2005 - 2:44:34 PM
Last modification on : Friday, February 26, 2021 - 3:28:04 PM
Long-term archiving on: : Friday, April 2, 2010 - 7:28:24 PM




Yann Zimmermann, Diana Toma. Component Reuse in B Using ACL2. ZB Formal Specification and Development in Z and B - 4th International Conference of B and Z Users - ZB 2005, Apr 2005, University of Surrey, Guildford, UK, pp.280-299, ⟨10.1007/b135596⟩. ⟨inria-00000755⟩



Record views


Files downloads