SourceForge has been redesigned. Learn more.
Close

Diff of /web/entries/RIPEMD-160-SPARK.shtml [2b3dd4] .. [c0ebd3]  Maximize  Restore

Switch to side-by-side view

--- a/web/entries/RIPEMD-160-SPARK.shtml
+++ b/web/entries/RIPEMD-160-SPARK.shtml
@@ -39,7 +39,7 @@
     <tr><td class="datahead" valign="top">Abstract:</td>
         <td class="abstract">
 
-Functional Specification of the cryptographic hash-function RIPEMD-160 in Isabelle/HOL. Implementation in SPARK/ADA. Verification of its functional correctness with proofs for the verification conditions generated by the static-analysis toolset of SPARK, translated to Isabelle/HOL.
+This work presents a verification of an implementation in SPARK/ADA of the cryptographic hash-function RIPEMD-160. A functional specification of RIPEMD-160 is given in Isabelle/HOL. Proofs for the verification conditions generated by the static-analysis toolset of SPARK certify the functional correctness of the implementation.
         </td></tr>
 
     <tr><td class="datahead">License:</td>