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

C++compiler verificationdata representationempty base classesmultiple inheritanceobject identityobject layout

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) 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)

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)

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

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)