Reasoning about memory layouts

DOI10.1007/s10703-010-0098-5zbMath1211.68086OpenAlexW2132122557MaRDI QIDQ633298

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

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

Related Items (1)

Reasoning about memory layouts

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Reasoning about memory layouts
• Isabelle. A generic theorem prover
• Proving pointer programs in higher-order logic
• Effective interactive proofs for higher-order imperative programs
• Verification of the Schorr-Waite Algorithm – From Trees to Graphs
• A Formalisation of Smallfoot in HOL
• Lightweight Separation
• Local Theory Specifications in Isabelle/Isar
• Automated verification of practical garbage collectors
• Context Aware Calculation and Deduction
• Shape Analysis for Composite Data Structures
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Reasoning about memory layouts