diff --git a/chap-intro.tex b/chap-intro.tex index 55387df8..895870f0 100644 --- a/chap-intro.tex +++ b/chap-intro.tex @@ -1096,6 +1096,11 @@ \section{Publications} model building on CHERI to secure mainstream and complex embedded software systems~\cite{UCAM-CL-TR-976}. +\item Kayvan Memarian's PhD dissertation, \citetitleit{UCAM-CL-TR-981}, + describes Cerberus, an executable model for a substantial fragment + of C11 expressed as a translation to a purpose-built language called + Core~\cite{UCAM-CL-TR-981}. + \item Peter Rugg's PhD dissertation, \citetitleit{UCAM-CL-TR-984}, describes the implementation of CHERI on three RISC-V microarchitectures as well as the refinement of support for temporal memory diff --git a/cheri.bib b/cheri.bib index e7a1ce19..104958ab 100644 --- a/cheri.bib +++ b/cheri.bib @@ -16699,6 +16699,17 @@ @TechReport{UCAM-CL-TR-976 number = {UCAM-CL-TR-976} } +@TechReport{UCAM-CL-TR-981, + author = {Memarian, Kayvan}, + title = {{The Cerberos C semantics}}, + year = 2023, + month = may, + url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-981.pdf}, + institution = {University of Cambridge, Computer Laboratory}, + doi = {10.48456/tr-981}, + number = {UCAM-CL-TR-981} +} + @TechReport{UCAM-CL-TR-982, author = {Watson, Robert N. M. and Barnes, Graeme and Clarke, Jessica and Grisenthwaite, Richard and Sewell, Peter and Moore,