diff options
| -rw-r--r-- | proof.tex | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -1,6 +1,6 @@ -\section{Semantics Preservation Proof of Translation}\label{sec:proof} +\section{Correctness Proof}\label{sec:proof} -\JW{That's quite a hard-to-parse section heading; I'd go for something simpler like `Correctness Proof' or `Proving Correctness'} +%\JW{That's quite a hard-to-parse section heading; I'd go for something simpler like `Correctness Proof' or `Proving Correctness'} Now that the Verilog semantics have been adapted to the CompCert model, we are in a position to formally prove the correctness of our C-to-Verilog compilation. This section describes the main correctness theorem that was proven and the key ideas in the proof. The full Coq proof is available online~\cite{yann_herklotz_2021_5093839}. |