Verified runtime assertion checking for memory properties

DOI10.1007/978-3-030-50995-8_6zbMATH Open1511.68083MaRDI QIDQ6487262FDOQ6487262

Authors: Nikolai Kosmatov, F. Loulergue, Julien Signoles 

Publication date: 9 November 2022

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• 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
• 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
• 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)