Sound runtime assertion checking for memory properties via program transformation

DOI10.1145/3605951MaRDI QIDQ7028282zbMATH OpenFDO

Authors Nikolai Kosmatov, F. Loulergue, Julien Signoles

Publication date 12 February 2025

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3605951

zbMATH Keywords

memory modelsoundness proofruntime assertion checkingmemory-related properties

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• scientific article; zbMATH DE number 1214924 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• A Why3 proof of GMP algorithms
• A formally verified compiler back-end
• Avoiding exponential explosion: generating compact verification conditions
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Mechanized semantics for the clight subset of the C language
• Producing certified functional code from inductive specifications
• Verified runtime assertion checking for memory properties

This page was built for publication: Sound runtime assertion checking for memory properties via program transformation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7028282)