## Diff of /thys/RIPEMD-160-SPARK/document/root.tex[2b3dd4] .. [c0ebd3]  Maximize  Restore

### Switch to side-by-side view

--- a/thys/RIPEMD-160-SPARK/document/root.tex
+++ b/thys/RIPEMD-160-SPARK/document/root.tex
@@ -38,12 +38,7 @@
\maketitle

\begin{abstract}
-  Functional Specification of the cryptographic hash-function RIPEMD-160
-  \cite{ripemd} in Isabelle/HOL \cite{LNCS2283}. Verification of the functional
-  correctness of an implementation in SPARK/ADA \cite{highintegritysoftware}
-  with proofs for the verification conditions generated by the static-analysis
-  toolset of SPARK, translated to Isabelle/HOL with
-  a modified version of Victor-0.8.0\cite{vct}.
+This work presents a verification of an implementation in SPARK/ADA \cite{highintegritysoftware} of the cryptographic hash-function RIPEMD-160. A functional specification of RIPEMD-160 \cite{ripemd} is given in Isabelle/HOL \cite{LNCS2283}. Proofs for the verification conditions generated by the static-analysis toolset of SPARK certify the functional correctness of the implementation. The verification conditions are translated to Isabelle/HOL with a modified version of Victor-0.8.0 \cite{vct}.
\end{abstract}

\tableofcontents