< Retour au sommaire

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

Louis Gauthier le

Lieu: Salle 1073

Suivre en visio

Abstract

ACSL is a behavioral interface specification language for C. It is used by Frama-C, a framework including several formal methods-based techniques 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, interpretations of the semantics by developers and users.

This presentation is a first step to solve this issue by formalizing a subset of the ACSL specification language in Coq. This semantics is based on Krebbers’semantics of C. The paper focuses on two features: an equality for structures and unions, which are comparable in ACSL, contrary to C, and a logic for handling underspecified terms and predicates that the total lo ic of ACSL let us manipulate. Finally, we also provide a few properties of our formal semantics.