High-Level Program Properties in Frama-C: Definition, Verification and Deduction

Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Pascale Le Gall

doi:10.1007/978-3-031-75380-0_10

High-Level Program Properties in Frama-C: Definition, Verification and Deduction

Virgile Robles
, Nikolai Kosmatov
, Virgile Prevosto
, Pascale Le Gall

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

In deductive verification of software, a contract is typically associated to each function and the implementation is shown to respect it. Such contracts for C programs can be expressed in the ACSL specification language. However, high-level (or global) program properties, in particular security properties, cannot be conveniently expressed as function contracts. This paper provides an overview of recent efforts to specify and verify global program properties in the Frama-C verification platform using a dedicated Frama-C plug-in called MetAcsl. Its verification approach relies on a translation of high-level properties into low-level ACSL annotations inserted in relevant program locations, followed by the verification of the resulting annotations. While this approach is expressive and powerful—and has already been effectively used in industrial applications—it can also be costly in terms of the number of the resulting low-level annotations. Deduction of high-level properties from other ones and from other annotations is thus desired. We discuss initial work on deduction of high-level properties and outline further research perspectives in this area.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification - 12th International Symposium, ISoLA 2024, Proceedings
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	159-177
Number of pages	19
ISBN (Print)	9783031753794
DOIs	https://doi.org/10.1007/978-3-031-75380-0_10
Publication status	Published - 1 Jan 2025
Externally published	Yes
Event	12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024 - Crete, Greece Duration: 27 Oct 2024 → 31 Oct 2024

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	15221 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024
Country/Territory	Greece
City	Crete
Period	27/10/24 → 31/10/24

Keywords

Deductive verification
Formal specification
Frama-C
High-level properties
MetAcsl

Access to Document

10.1007/978-3-031-75380-0_10

Cite this

Robles, V., Kosmatov, N., Prevosto, V., & Le Gall, P. (2025). High-Level Program Properties in Frama-C: Definition, Verification and Deduction. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification - 12th International Symposium, ISoLA 2024, Proceedings (pp. 159-177). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) ; Vol. 15221 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-75380-0_10

Robles, Virgile ; Kosmatov, Nikolai ; Prevosto, Virgile et al. / High-Level Program Properties in Frama-C : Definition, Verification and Deduction. Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification - 12th International Symposium, ISoLA 2024, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Springer Science and Business Media Deutschland GmbH, 2025. pp. 159-177 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) ).

@inproceedings{5cc6648c0b3e403fab02d8e32aa5394e,

title = "High-Level Program Properties in Frama-C: Definition, Verification and Deduction",

abstract = "In deductive verification of software, a contract is typically associated to each function and the implementation is shown to respect it. Such contracts for C programs can be expressed in the ACSL specification language. However, high-level (or global) program properties, in particular security properties, cannot be conveniently expressed as function contracts. This paper provides an overview of recent efforts to specify and verify global program properties in the Frama-C verification platform using a dedicated Frama-C plug-in called MetAcsl. Its verification approach relies on a translation of high-level properties into low-level ACSL annotations inserted in relevant program locations, followed by the verification of the resulting annotations. While this approach is expressive and powerful—and has already been effectively used in industrial applications—it can also be costly in terms of the number of the resulting low-level annotations. Deduction of high-level properties from other ones and from other annotations is thus desired. We discuss initial work on deduction of high-level properties and outline further research perspectives in this area.",

keywords = "Deductive verification, Formal specification, Frama-C, High-level properties, MetAcsl",

author = "Virgile Robles and Nikolai Kosmatov and Virgile Prevosto and \{Le Gall\}, Pascale",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.; 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024 ; Conference date: 27-10-2024 Through 31-10-2024",

year = "2025",

month = jan,

day = "1",

doi = "10.1007/978-3-031-75380-0\_10",

language = "English",

isbn = "9783031753794",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) ",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "159--177",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification - 12th International Symposium, ISoLA 2024, Proceedings",

}

Robles, V, Kosmatov, N, Prevosto, V & Le Gall, P 2025, High-Level Program Properties in Frama-C: Definition, Verification and Deduction. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification - 12th International Symposium, ISoLA 2024, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) , vol. 15221 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 159-177, 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024, Crete, Greece, 27/10/24. https://doi.org/10.1007/978-3-031-75380-0_10

High-Level Program Properties in Frama-C: Definition, Verification and Deduction. / Robles, Virgile; Kosmatov, Nikolai; Prevosto, Virgile et al.
Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification - 12th International Symposium, ISoLA 2024, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Springer Science and Business Media Deutschland GmbH, 2025. p. 159-177 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) ; Vol. 15221 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - High-Level Program Properties in Frama-C

T2 - 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024

AU - Robles, Virgile

AU - Kosmatov, Nikolai

AU - Prevosto, Virgile

AU - Le Gall, Pascale

N1 - Publisher Copyright: © The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.

PY - 2025/1/1

Y1 - 2025/1/1

N2 - In deductive verification of software, a contract is typically associated to each function and the implementation is shown to respect it. Such contracts for C programs can be expressed in the ACSL specification language. However, high-level (or global) program properties, in particular security properties, cannot be conveniently expressed as function contracts. This paper provides an overview of recent efforts to specify and verify global program properties in the Frama-C verification platform using a dedicated Frama-C plug-in called MetAcsl. Its verification approach relies on a translation of high-level properties into low-level ACSL annotations inserted in relevant program locations, followed by the verification of the resulting annotations. While this approach is expressive and powerful—and has already been effectively used in industrial applications—it can also be costly in terms of the number of the resulting low-level annotations. Deduction of high-level properties from other ones and from other annotations is thus desired. We discuss initial work on deduction of high-level properties and outline further research perspectives in this area.

AB - In deductive verification of software, a contract is typically associated to each function and the implementation is shown to respect it. Such contracts for C programs can be expressed in the ACSL specification language. However, high-level (or global) program properties, in particular security properties, cannot be conveniently expressed as function contracts. This paper provides an overview of recent efforts to specify and verify global program properties in the Frama-C verification platform using a dedicated Frama-C plug-in called MetAcsl. Its verification approach relies on a translation of high-level properties into low-level ACSL annotations inserted in relevant program locations, followed by the verification of the resulting annotations. While this approach is expressive and powerful—and has already been effectively used in industrial applications—it can also be costly in terms of the number of the resulting low-level annotations. Deduction of high-level properties from other ones and from other annotations is thus desired. We discuss initial work on deduction of high-level properties and outline further research perspectives in this area.

KW - Deductive verification

KW - Formal specification

KW - Frama-C

KW - High-level properties

KW - MetAcsl

UR - https://www.scopus.com/pages/publications/85208536227

U2 - 10.1007/978-3-031-75380-0_10

DO - 10.1007/978-3-031-75380-0_10

M3 - Conference contribution

AN - SCOPUS:85208536227

SN - 9783031753794

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 159

EP - 177

BT - Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification - 12th International Symposium, ISoLA 2024, Proceedings

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 27 October 2024 through 31 October 2024

ER -

Robles V, Kosmatov N, Prevosto V, Le Gall P. High-Level Program Properties in Frama-C: Definition, Verification and Deduction. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification - 12th International Symposium, ISoLA 2024, Proceedings. Springer Science and Business Media Deutschland GmbH. 2025. p. 159-177. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) ). doi: 10.1007/978-3-031-75380-0_10