Add outline of slides.

[libguestfs-talks.git] / 2020-frama-c / 1000-introduction.html

diff --git a/2020-frama-c/1000-introduction.html b/2020-frama-c/1000-introduction.html
new file mode 100644 (file)
index 0000000..991dc59
--- /dev/null
+++ b/2020-frama-c/1000-introduction.html
@@ -0,0 +1,21 @@
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<link rel="stylesheet" href="style.css" type="text/css"/>
+<script src="code.js" type="text/javascript"></script>
+
+<div id="titlepage">
+  <p class="title">
+    Formally proving tiny bits of qemu using Frama-C
+  </p>
+
+  <p class="author">
+    Richard W.M. Jones <small>(rjones @ redhat.com)</small> <br/>
+    <small>Monday November 16th, 2020</small>
+  </p>
+
+  <p class="abstract">
+    <b>Formal verification</b> of software proves that the software is
+    mathematically correct with respect to its specification.
+    <b>Frama-C</b> is an open source modular framework for formal verification
+    of programs written in C.
+  </p>
+</div>