Treffer: A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification

Title:
A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification
Authors:
Louis Gauthier, Virgile Prevosto, Julien Signoles
Contributors:
CEA, Contributeur MAP
Source:
Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE). :100-110
Publisher Information:
ACM, 2024.
Publication Year:
2024
Subject Terms:
Formal Specification Language, Coq Proof Assistant, Formal Semantics, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
Document Type:
Fachzeitschrift Article<br />Conference object
File Description:
application/pdf
DOI:
10.1145/3644033.3644380
Access URL:
https://cea.hal.science/cea-04480238v1
https://doi.org/10.1145/3644033.3644380
https://cea.hal.science/cea-04480238v1/document
Rights:
URL: https://www.acm.org/publications/policies/copyright_policy#Background
Accession Number:
edsair.doi.dedup.....05d6a1ba22373b84c0b49062b50a937c
Database:
OpenAIRE

Weitere Informationen

ACSL is a behavioral interface specification language for C. It is usedby Frama-C, a framework including several formal methods-basedtechniques for verifying C code with respect to ACSL annotations.Currently, there is no formal definition of the ACSL semantics,which may lead to different, possibly inconsistent, interpretationsof the semantics by developers and users. This paper is a first stepto solve this issue by formalizing a subset of the ACSL specificationlanguage in Coq. This semantics is based on Krebbers’ semanticsof C. The paper focuses on two features: an equality for structuresand unions, which are comparable in ACSL, contrary to C, anda logic for handling underspecified terms and predicates that thetotal logic of ACSL let us manipulate. Finally, we also provide a fewproperties of our formal semantics.