ACSL (ANSI/ISO C Specification Language)

Concept

ACSL is a behavioral specification language for C, based on Hoare-style axiomatic semantics, that is used as the annotation language of the Frama-C framework for deductive verification of C programs.

First seen 6/7/2026

Last seen 6/7/2026

Evidence 1 chunks

Wiki v1

WIKI

ACSL (ANSI/ISO C Specification Language)

Overview

ACSL (ANSI/ISO C Specification Language) is a formal specification language for the C programming language. It is based on an axiomatic semantics for C in the style of Hoare logic, and is the primary language used to annotate C source code for the Frama-C framework — an extensible set of interoperable program analyzers for C.

Semantics and Design Rationale

ACSL provides a Hoare-logic / weakest-precondition foundation for expressing properties of C programs (preconditions, postconditions, loop invariants, predicates over memory, etc.). Most of the analyzers bundled in Frama-C consume ACSL annotations as the formal contract format that drives deductive reasoning about C code.

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

1 connections

Frama-C ← uses 95% 1e

Frama-C modules rely on ACSL specification language

LINKED ENTITIES

2 links

Frama-C USES Extracted graph relationship

CompCert ALTERNATIVE_APPROACH Evidence explicitly contrasts ACSL/Frama-C's axiomatic-semantics approach with CompCert's operational semantics of a C subset, used in Coq, when discussing how to certify an ARM simulator written in C.

CITATIONS

5 sources

5 citations — click to expand

[1] ACSL is a specification language for C based on axiomatic semantics, and is the language used by Frama-C analyzers. Towards Verified Faithful Simulation (SETTA 2015)

[2] Frama-C builds on the Why platform, compiling ACSL-annotated C into Why's intermediate language, from which a VC generator emits obligations dispatched to automatic and interactive provers (e.g., Coq). Towards Verified Faithful Simulation (SETTA 2015)

[3] ACSL with Frama-C's WP plugin and Alt-Ergo has been applied to formalize and partially verify low-level requirements from a DO-178C-compliant avionics project, in the context of the DO-333 formal-methods supplement. An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Project

[4] Frama-C's WP plugin, in combination with multiple SMT solvers, is used to assess automatically generated ACSL annotations (from rule-based scripts, the RTE plugin, and LLMs such as DeepSeek-V3.2, GPT-5.2, and OLMo 3.1 32B Instruct) on a filtered subset of the CASP benchmark. Evaluating LLM-Generated ACSL Annotations for Formal Verification

[5] Rule-based ACSL annotation strategies are reported as more reliable for verification success than LLM-based one-shot annotation strategies, which exhibit more variable performance. Evaluating LLM-Generated ACSL Annotations for Formal Verification