Skip to main content
CSIRO Logo Data 61 logo

A formal semantics for c++

Authors

Michael Norrish

NICTA

Abstract

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

  @techreport{Norrish_07:tr,
    month            = nov,
    institution      = {NICTA},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/1203.pdf},
    author           = {Norrish, Michael},
    year             = {2007},
    title            = {A Formal Semantics for C++},
    address          = {Canberra}
  }

Download