Reasoning about memory layouts

DOI10.1007/S10703-010-0098-5MaRDI QIDQ633298zbMATH OpenOpenAlexFDO

Authors Holger Gast

Publication date 31 March 2011

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-010-0098-5

zbMATH Keywords

C verificationlow-level memory modelspointer programsSchorr-Waite graph traversal

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Region analysis for deductive verification of C programs
• Types, bytes, and separation logic
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• A shape graph logic and a shape system
• Proving pointer programs in higher-order logic.

Cites work

• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• A Formalisation of Smallfoot in HOL
• Automated verification of practical garbage collectors
• Context Aware Calculation and Deduction
• Effective interactive proofs for higher-order imperative programs
• Isabelle. A generic theorem prover
• Lightweight Separation
• Local Theory Specifications in Isabelle/Isar
• Logic for Programming, Artificial Intelligence, and Reasoning
• Proving pointer programs in higher-order logic
• Reasoning about memory layouts
• Shape Analysis for Composite Data Structures
• Verification of the Schorr-Waite algorithm -- from trees to graphs

Cited in

(4)

• Region analysis for deductive verification of C programs
• Formal verification of object layout for C++ multiple inheritance
• Reasoning about memory layouts
• scientific article; zbMATH DE number 1760123 (Why is no real title available?)

Describes a project that uses

Uses Software

• STL
• Smallfoot
• Boogie
• Caduceus
• Isar
• Why3
• KRAKATOA
• Isabelle
• ACL2

This page was built for publication: Reasoning about memory layouts

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