Trustworthy Systems

A formal semantics for c++


Michael Norrish



This document describes a formal operational model of the dynamic semantics of much of the C++ language (as specified in the ISO Standard). The formal model was developed in the HOL theorem-prover, providing additional guarantees as to its good sense. This report presents and explains extracts from the mechanised source-code that was fed to HOL.

This work was performed under funding from QinetiQ’s Systems Assurance Group under the UK MOD Output 3a research project entitled Robust Languages.

BibTeX Entry

    month            = nov,
    institution      = {NICTA},
    paperurl         = {},
    author           = {Norrish, Michael},
    year             = {2007},
    title            = {A Formal Semantics for C++},
    address          = {Canberra}