FormaliSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal
co-located with ICSE 2024
Mon 15 Apr 2024 11:00 - 11:30 at Eugénio de Andrade - Theorem proving and applications Chair(s): Claire Dross

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 paper 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 logic of ACSL let us manipulate. Finally, we also provide a few properties of our formal semantics.

Mon 15 Apr

Displayed time zone: Lisbon change

11:00 - 12:30
Theorem proving and applicationsFormaliSE 2024 at Eugénio de Andrade
Chair(s): Claire Dross AdaCore
11:00
30m
Talk
A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification
FormaliSE 2024
Louis Gauthier Université Paris-Saclay, CEA, List, Virgile Prevosto Université Paris-Saclay, CEA, List, Julien Signoles Université Paris-Saclay, CEA, List
11:30
30m
Talk
Formally Verified Interval Arithmetic and Its Application to Program Verification
FormaliSE 2024
Achim D. Brucker University of Exeter, Teddy Cameron-Burke University of Exeter, Amy Stell University of Exeter
12:00
30m
Talk
Towards Verifiable Multi-Agent Interaction Pattern Specification
FormaliSE 2024
Alberto Tagliaferro Politecnico di Milano, Italy, Livia Lestingi DEIB, Politecnico di Milano, Matteo Rossi Politecnico di Milano