Sound Runtime Assertion Checking for Memory Properties via Program Transformation

Dara Ly; Nikolai Kosmatov; Frédéric Loulergue; Julien Signoles

doi:10.1145/3605951

Sound Runtime Assertion Checking for Memory Properties via Program Transformation

Dara Ly
, Nikolai Kosmatov
, Frédéric Loulergue
, Julien Signoles

Research output: Contribution to journal › Article › peer-review

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 article presents a formalization of a program transformation technique for RAC of memory properties for a representative language with pointers and memory operations, including dynamic allocation and deallocation. The generated program instrumentation relies on an axiomatized observation memory model, which is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.

Original language	English
Article number	4
Journal	Formal Aspects of Computing
Volume	36
Issue number	1
DOIs	https://doi.org/10.1145/3605951
Publication status	Published - 20 Mar 2024
Externally published	Yes

Keywords

Runtime assertion checking
memory model
memory-related properties
soundness proof

Access to Document

10.1145/3605951

Cite this

@article{e6dd0f8ba1cc423abf5f486de1ae96e9,

title = "Sound Runtime Assertion Checking for Memory Properties via Program Transformation",

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 article presents a formalization of a program transformation technique for RAC of memory properties for a representative language with pointers and memory operations, including dynamic allocation and deallocation. The generated program instrumentation relies on an axiomatized observation memory model, which is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.",

keywords = "Runtime assertion checking, memory model, memory-related properties, soundness proof",

author = "Dara Ly and Nikolai Kosmatov and Fr{\'e}d{\'e}ric Loulergue and Julien Signoles",

note = "Publisher Copyright: {\textcopyright} 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.",

year = "2024",

month = mar,

day = "20",

doi = "10.1145/3605951",

language = "English",

volume = "36",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

number = "1",

}

TY - JOUR

T1 - Sound Runtime Assertion Checking for Memory Properties via Program Transformation

AU - Ly, Dara

AU - Kosmatov, Nikolai

AU - Loulergue, Frédéric

AU - Signoles, Julien

PY - 2024/3/20

Y1 - 2024/3/20

N2 - 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 article presents a formalization of a program transformation technique for RAC of memory properties for a representative language with pointers and memory operations, including dynamic allocation and deallocation. The generated program instrumentation relies on an axiomatized observation memory model, which is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.

AB - 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 article presents a formalization of a program transformation technique for RAC of memory properties for a representative language with pointers and memory operations, including dynamic allocation and deallocation. The generated program instrumentation relies on an axiomatized observation memory model, which is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.

KW - Runtime assertion checking

KW - memory model

KW - memory-related properties

KW - soundness proof

U2 - 10.1145/3605951

DO - 10.1145/3605951

M3 - Article

AN - SCOPUS:85189163153

SN - 0934-5043

VL - 36

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 1

M1 - 4

ER -

Sound Runtime Assertion Checking for Memory Properties via Program Transformation

Abstract

Keywords

Access to Document

Fingerprint

Cite this