Update on Overleaf.

1 files changed, 3 insertions, 2 deletions

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index e441688..9933ae8 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -66,6 +66,7 @@ escapeinside=||,
 \newcommand\MP[2][]{\st{#1}\Comment{blue!50!magenta}{MP}{#2}}
 
 \newcommand\JWchanged[1]{\textcolor{red!75!black}{#1}}
+\newcommand\YHchanged[1]{\textcolor{blue!50!green}{#1}}
 
 \newcommand\vericert{Vericert}
 \newcommand\vericertfun{Vericert-Fun}
@@ -122,8 +123,8 @@ Developing software within a proof assistant like Coq is widely held to be the g
 It transforms its input through a series of ten intermediate languages before generating the final output. 
 %This design ensures that each individual pass remains relatively simple and hence feasible to prove correct.
 The correctness proof of the entire compiler is formed by composing the correctness proofs of each of those passes. 
-That the Csmith compiler testing tool~\cite{csmith} has found hundreds of bugs in GCC and LLVM but none in (the verified parts of) CompCert is a testament to the reliability of this development approach. 
-That said, we cannot guarantee \vericertfun{} designs will never go wrong, because of fallible components not covered by the theorem, such as the synthesis toolchain~\cite{verismith} and the FPGA itself.
+\YHchanged{That the Csmith compiler testing tool}~\cite{csmith} has found hundreds of bugs in GCC and LLVM but none in (the verified parts of) CompCert is a testament to the reliability of this development approach. 
+\YHchanged{However, we} cannot guarantee \vericertfun{} designs will never go wrong, because of fallible components not covered by the theorem, such as the synthesis toolchain~\cite{verismith} and the FPGA itself.
  
 \paragraph{The \vericert{} verified HLS tool}