2020-frama-c/1000-introduction.html

   1 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
   2 <link rel="stylesheet" href="style.css" type="text/css"/>
   3 <script src="code.js" type="text/javascript"></script>
   4
   5 <div id="titlepage">
   6   <p class="title">
   7     Formally proving tiny bits of qemu using Frama-C
   8   </p>
   9
  10   <p class="author">
  11     Richard W.M. Jones <small>(rjones @ redhat.com)</small> <br/>
  12     <small>Monday November 16th, 2020</small>
  13   </p>
  14
  15   <p class="abstract">
  16     <b>Formal verification</b> of software proves that the software is
  17     mathematically correct with respect to its specification.
  18     <b>Frama-C</b> is an open source modular framework for formal verification
  19     of programs written in C.
  20   </p>
  21 </div>