Carben, AndreasGu, LiangliangHartig, KerstinPohl, HansSoto, JuanVöllinger, KimBurghardt, JochenJochenBurghardtGerlach, JensJensGerlachLapawczyk, TimonTimonLapawczyk2022-03-072022-03-072015https://publica.fraunhofer.de/handle/publica/297476This report provides various examples for the formal specification, implementation, and deductive verification of C programs using the ANSI/ISO-C Specification Language (ACSL) and the WP plug-in of Frama-C (Framework for Modular Analysis of C programs). The report at hand has been revised and refers to the Sodium release from March 2015 of Frama-C.enformal verification of C softwareFrama-C004report