Mostly finished first draft of intro

1 files changed, 8 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index b3c9846..8bbcf5a 100644
--- a/main.tex
+++ b/main.tex
@@ -187,7 +187,14 @@ CompCert~\cite{leroy06_formal_certif_compil_back_end} is a C compiler that has b
 
 %% Contributions of paper
 
-Using CompCert, we can therefore build a fully verified high-level synthesis tool written in Coq
+In this paper we describe a fully verified high-level synthesis tool called CoqUp, which adds a Verilog backend to CompCert and proves that the behaviour of the C code does not change according to existing Verilog semantics.  The main contributions of the paper are the following:
+
+\begin{itemize}
+  \item Proof by simulation mechanised in Coq between CompCert's intermediate language and Verilog.
+  \item Description of the Verilog semantics used to integrate it into CompCert's model.
+\end{itemize}
+
+CoqUp is open source and is hosted on Github\footnote{https://github.com/ymherklotz/coqup}.
 
 \section{Background}