At the Brazilian conference on formal methods @SBMF 2025 (2–5 December, Recife), the @Metrópole Digital Institute – IMD/UFRN and CLEARSY present their work on the formal verification of C code generated from a formal model in B language.
In our article entitled “Bridging the B-Method and ACSL”, we show how to automatically generate ACSL assertions from B models in order to verify, with Frama-C, that the C code retains the formal properties initially defined.
This approach combines formal modelling and static analysis and ensures that critical embedded code meets its safety requirements. A case study illustrates its effectiveness.
By combining mathematical rigour with modern proofs and tools, CLEARSY continues its commitment to operational safety and security based on innovation and formal methods.