 |
Conference papers
Verified Runtime Assertion Checking for Memory Properties
Abstract : Runtime Assertion Checking (RAC) for expressive specification languages is a non-trivial verification task, that becomes even more complex for memory-related properties of imperative languages with dynamic memory allocation. It is important to ensure the soundness of RAC verdicts, in particular when RAC reports the absence of failures for execution traces. This paper presents a formalization of a program transformation technique for RAC of memory properties for a representative language with memory operations. It includes an observation memory model that is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.
Cited literature [36 references]
https://hal-cea.archives-ouvertes.fr/cea-02879211
Contributor : Dara Ly Connect in order to contact the contributor
Submitted on : Tuesday, June 23, 2020 - 3:56:10 PM
Last modification on : Wednesday, November 3, 2021 - 7:32:29 AM
Long-term archiving on: : Thursday, September 24, 2020 - 6:05:36 PM
Contributor : Dara Ly Connect in order to contact the contributor
Submitted on : Tuesday, June 23, 2020 - 3:56:10 PM
Last modification on : Wednesday, November 3, 2021 - 7:32:29 AM
Long-term archiving on: : Thursday, September 24, 2020 - 6:05:36 PM
File
TAP_2020_paper_7.pdf
Files produced by the author(s)