• English
  • Deutsch
  • Log In
    or
  • Research Outputs
  • Projects
  • Researchers
  • Institutes
  • Statistics
Repository logo
Fraunhofer-Gesellschaft
  1. Home
  2. Fraunhofer-Gesellschaft
  3. Buch
  4. ACSL by example
 
  • Details
  • Full
Options
2015
Bericht
Titel

ACSL by example

Titel Supplements
Towards a verified C standard library. Version 11.11 for Frama-C (Sodium), June 2015
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.
Author(s)
Burghardt, Jochen
Fraunhofer-Institut für Offene Kommunikationssysteme FOKUS
Gerlach, Jens
Fraunhofer-Institut für Offene Kommunikationssysteme FOKUS
Lapawczyk, Timon
Fraunhofer-Institut für Offene Kommunikationssysteme FOKUS
Beteiligt
Carben, Andreas
Gu, Liangliang
Hartig, Kerstin
Pohl, Hans
Soto, Juan
Völlinger, Kim
Verlag
Fraunhofer FOKUS
Verlagsort
Berlin
Project(s)
STANCE
Funder
European Commission EC
Thumbnail Image
Language
Englisch
google-scholar
FOKUS
Tags
  • formal verification o...

  • Frama-C

  • Cookie settings
  • Imprint
  • Privacy policy
  • Api
  • Send Feedback
© 2022