Skip to Main content Skip to Navigation
Conference papers

Soundness of a Dataflow Analysis for Memory Monitoring

Abstract : An important concern addressed by runtime verification tools for C code is related to detecting memory errors. It requires to monitor some properties of memory locations (e.g., their validity and initialization) along the whole program execution. Static analysis based optimizations have been shown to significantly improve the performances of such tools by reducing the monitoring of irrelevant locations. However, soundness of the verdict of the whole tool strongly depends on the soundness of the underlying static analysis technique. This paper tackles this issue for the dataflow analysis used to optimize the E-ACSL runtime assertion checking tool. We formally define the core dataflow analysis used by E-ACSL and prove its soundness.
Document type :
Conference papers
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-02283406
Contributor : Dara Ly <>
Submitted on : Tuesday, September 10, 2019 - 5:53:47 PM
Last modification on : Monday, February 10, 2020 - 6:12:33 PM

File

2018_hilt.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-02283406, version 1

Citation

Dara Ly, Nikolai Kosmatov, Julien Signoles, Frédéric Loulergue. Soundness of a Dataflow Analysis for Memory Monitoring. HILT 2018 Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems, Nov 2018, Boston, United States. ⟨cea-02283406⟩

Share

Metrics

Record views

71

Files downloads

85