TY - GEN
T1 - The e-ACSL perspective on runtime assertion checking
AU - Signoles, Julien
N1 - Publisher Copyright:
© 2021 ACM.
PY - 2021/7/12
Y1 - 2021/7/12
N2 - 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.
AB - 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.
KW - Behavioral Interface Specification Language
KW - Combination of Static and Dynamic Analyses
KW - Runtime Assertion Checking
KW - Source Code Generation
U2 - 10.1145/3464974.3468451
DO - 10.1145/3464974.3468451
M3 - Conference contribution
AN - SCOPUS:85111411455
T3 - VORTEX 2021 - Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution, co-located with ECOOP/ISSTA 2021
SP - 8
EP - 12
BT - VORTEX 2021 - Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution, co-located with ECOOP/ISSTA 2021
A2 - Ahrendt, Wolfgang
A2 - Ancona, Davide
A2 - Francalanza, Adrian
PB - Association for Computing Machinery, Inc
T2 - 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution, VORTEX 2021, co-located with ECOOP/ISSTA 2021
Y2 - 12 July 2021
ER -