Verified runtime assertion checking for memory properties

DOI10.1007/978-3-030-50995-8_6MaRDI QIDQ6487262zbMATH OpenFDO

Authors Nikolai Kosmatov, F. Loulergue, Julien Signoles

Publication date 9 November 2022

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Sufficient Preconditions for Modular Assertion Checking
• Runtime Checking for Separation Logic
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Model checking dynamic memory allocation in operating systems
• Sound modular verification of C code executing in an unverified context

Cites work

• scientific article; zbMATH DE number 108549 (Why is no real title available?)
• Formal verification of a C-like memory model and its uses for verifying program transformations
• How to get an efficient yet verified arbitrary-precision integer library
• 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

Cited in

(2)

• Abstract interpretation of recursive logic definitions for efficient runtime assertion checking
• Practical run-time checking via unobtrusive property caching

This page was built for publication: Verified runtime assertion checking for memory properties

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