Fix more dead links

+ minor cosmetic changes in documentation

_posts/2011-03-03-This-time-for-real-verifying-function-cosine.html

@@ -22,7 +22,7 @@ summary:
 </pre> 
 <p>Next  I arranged to have the value analysis repeatedly analyze these lines with bounds passed to <code>Frama_C_double_interval</code> that  taken together  cover entirely the range from 0 to π/4. I will not say how I did  because it is not very interesting. Besides  the method I used is convenient enough to discourage someone from writing an Emacs Lisp macro to generate sub-division assertions. That would be an unwanted side-effect: it in fact has complementary advantages with the would-be assertion generation macro that I recommend someone look into.</p> 
 <p>The verification used a few hours of CPU time (I did not try very hard to make it fast). One thing I did was adapt the input sub-interval width to the part of the curve that was being verified  from two millionths for inputs near zero to a quarter of a millionth for inputs near π/4.</p> 
-<p>During this experiment  I actually used the cosine implementation from <a href="http://lipforge.ens-lyon.fr/www/crlibm/" hreflang="en">CRlibm</a> as reference function. This library  incidentally developed at my alma mater  provides a number of fast <strong>and</strong> correctly rounded implementations for mathematical functions. 
+<p>During this experiment  I actually used the cosine implementation from <a href="https://github.com/taschini/crlibm" hreflang="en">CRlibm</a> as reference function. This library  incidentally developed at my alma mater  provides a number of fast <strong>and</strong> correctly rounded implementations for mathematical functions. 
 The value analysis was configured with the <code>-all-rounding-modes</code> option  so the results are guaranteed for arbitrary rounding modes  and are guaranteed even if the compiler uses supplemental precision for intermediate results (e.g. if the compiler uses the infamous 80-bit historial floating-point unit of Intel processors).</p> 
 <p>Here are the logs I obtained (warning: I did not make any file of that level of boringness publicly available since my PhD  plus these are really big  even after compression. Handle with care): <a href="/assets/img/blog/imported-posts/log1.gz">log1.gz</a> <a href="/assets/img/blog/imported-posts/log2.gz">log2.gz</a> <a href="/assets/img/blog/imported-posts/log3.gz">log3.gz</a> <a href="/assets/img/blog/imported-posts/log4.gz">log4.gz</a> <a href="/assets/img/blog/imported-posts/log5.gz">log5.gz</a> <a href="/assets/img/blog/imported-posts/log6.gz">log6.gz</a> <a href="/assets/img/blog/imported-posts/log7.gz">log7.gz</a> <a href="/assets/img/blog/imported-posts/log8.gz">log8.gz</a> <a href="/assets/img/blog/imported-posts/log9.gz">log9.gz</a> <a href="/assets/img/blog/imported-posts/log10.gz">log10.gz</a> <a href="/assets/img/blog/imported-posts/log11.gz">log11.gz</a> <a href="/assets/img/blog/imported-posts/log12.gz">log12.gz</a> <a href="/assets/img/blog/imported-posts/log13.gz">log13.gz</a> <a href="/assets/img/blog/imported-posts/log14.gz">log14.gz</a> <a href="/assets/img/blog/imported-posts/log15.gz">log15.gz</a>. To save you the bother of downloading even the first file  here is what the first three lines look like.</p> 
 <pre>[value] CC -0.0000000000000000 0.0000019073486328 0.9999999999981809 1.0000000000000002 0.9999999999981810 1.0000000000000000 OK