The E-ACSL Perspective on Runtime Assertion Checking
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.
Slides (Signoles.pdf) | 748KiB |
Mon 12 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
13:30 - 14:50 | |||
13:30 40mKeynote | The E-ACSL Perspective on Runtime Assertion Checking VORTEX Julien Signoles CEA LIST File Attached | ||
14:10 20mTalk | Towards Aggregate Monitoring of Spatio-temporal Properties VORTEX File Attached | ||
14:30 20mTalk | RM for Users’ Safety and Security in the Built Environment VORTEX Giorgio Audrito Università di Torino, Ferruccio Damiani University of Turin, Giuseppe Di Giuda , Silvia Meschini , Laura Pellegrini , Elena Seghezzi , Lavinia Chiara Tagliabue , Lorenzo Testa , Gianluca Torta File Attached |