Formal verification of object layout for C++ multiple inheritance

DOI10.1145/1926385.1926395MaRDI QIDQ5408532zbMATH OpenOpenAlexFDO

Authors Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy

Publication date 10 April 2014

Published in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-00674174/file/cpp-object-layout.pdf

zbMATH Keywords

data representationC++multiple inheritanceobject identitycompiler verificationempty base classesobject layout

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Quantifying and evaluating the space overhead for alternative C++ memory layouts
• A mechanized semantics for C++ object construction and destruction, with applications to resource management
• Reasoning about memory layouts
• Separation Logic for Multiple Inheritance
• A Framework for Formal Verification of Compiler Optimizations

Cited in

(4)

• A theory of platform-dependent low-level software
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Aliasing restrictions of C11 formalized in Coq
• A formal C memory model for separation logic

This page was built for publication: Formal verification of object layout for C++ multiple inheritance

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