C++ suffers from the Thin Air Problem, where the memory model witnesses behaviours which aren't allowed by the hardware or the compiler, and unwanted values can appear "out of thin air". There have been several candidate solutions to this. We are working to extend a concise but underdeveloped solution proposed by Jeffrey and Riely. This talk presents work in progress, including tool building in OCaml and Isabelle/HOL and model extension to support additional C++ features.
Cornwallis South West,
University of Kent,