Formal verification of object layout for C++ multiple inheritance

DOI10.1145/1926385.1926395zbMATH Open1284.68197OpenAlexW4230366227MaRDI QIDQ5408532FDOQ5408532

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

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

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)

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)