@inproceedings{c668a110bc1c42778e7126f9c9cabd49,
title = "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.",
author = "Dara Ly and Nikolai Kosmatov and Fr{\'e}d{\'e}ric Loulergue and Julien Signoles",
note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2020.; 14th International Conference on Tests and Proofs, TAP 2020, held as part of Software Technologies: Applications and Foundations, STAF 2020 ; Conference date: 22-06-2020 Through 23-06-2020",
year = "2020",
month = jan,
day = "1",
doi = "10.1007/978-3-030-50995-8\_6",
language = "English",
isbn = "9783030509941",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "100--121",
editor = "Wolfgang Ahrendt and Heike Wehrheim",
booktitle = "Tests and Proofs - 14th International Conference, TAP 2020, held as part of STAF 2020, Proceedings",
}