Skip to Main content Skip to Navigation
Conference papers

The E-ACSL Perspective on Runtime Assertion Checking

Julien Signoles 1
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : Runtime Assertion Checking (RAC) is the discipline of verifying program assertions at runtime, i.e. when executing the code. Nowadays, RAC usually relies on Behavioral Interface Specification Languages (BISL) à la Eiffel for writing powerful code specifications. Since now more than 20 years, several works have studied RAC. Most of them have focused on BISL. Some others have also considered combinations of RAC with others techniques, e.g. deductive verification (DV). Very few tackle RAC as a verification technique that soundly generates efficient code from formal annotations. Here, we revisit these three RAC's research areas by emphasizing the works done in E-Acsl, which is both a BISL and a RAC tool for C code. We also compare it to others languages and tools.
Complete list of metadata

https://hal-cea.archives-ouvertes.fr/cea-03313535
Contributor : Contributeur Map Cea Connect in order to contact the contributor
Submitted on : Wednesday, August 4, 2021 - 11:22:20 AM
Last modification on : Saturday, August 7, 2021 - 3:48:22 AM
Long-term archiving on: : Friday, November 5, 2021 - 6:31:17 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-01-23

Please log in to resquest access to the document

Identifiers

Citation

Julien Signoles. The E-ACSL Perspective on Runtime Assertion Checking. International Workshop on Verification and mOnitoring at Runtime EXecution, Jul 2021, (online), Denmark. https://doi.org/10.1145/3464974.3468451, ⟨10.1145/3464974.3468451⟩. ⟨cea-03313535⟩

Share

Metrics

Record views

36