Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance.
Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alexander Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, Peter Sewell
Browse the full ASPLOS paper archive.