• English
  • Deutsch
  • Log In
    Password Login
    Research Outputs
    Fundings & Projects
    Researchers
    Institutes
    Statistics
Repository logo
Fraunhofer-Gesellschaft
  1. Home
  2. Fraunhofer-Gesellschaft
  3. Buch
  4. ACSL by example
 
  • Details
  • Full
Options
2015
Report
Title

ACSL by example

Title Supplement
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  
Person Involved
Carben, Andreas
Gu, Liangliang
Hartig, Kerstin
Pohl, Hans
Soto, Juan
Völlinger, Kim
Publisher
Fraunhofer FOKUS
Publishing Place
Berlin
Project(s)
STANCE  
Funder
European Commission EC  
Language
English
Fraunhofer-Institut für Offene Kommunikationssysteme FOKUS  
Keyword(s)
  • formal verification of C software

  • Frama-C

  • Cookie settings
  • Imprint
  • Privacy policy
  • Api
  • Contact
© 2024