Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

ACSL by example

Towards a verified C standard library. Version 11.11 for Frama-C (Sodium), June 2015
 
: Burghardt, Jochen; Gerlach, Jens; Lapawczyk, Timon
: Carben, Andreas; Gu, Liangliang; Hartig, Kerstin; Pohl, Hans; Soto, Juan; Völlinger, Kim

Berlin: Fraunhofer FOKUS, 2015, 143 pp.
European Commission EC
FP7-ICT; 317753; STANCE
English
Report
Fraunhofer FOKUS ()
formal verification of C software; Frama-C

Abstract
This 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.

: http://publica.fraunhofer.de/documents/N-364387.html