A formal semantics for c++
Authors
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} }