some files orphaned

[helm.git] / helm / www / matita / theses.shtml

diff --git a/helm/www/matita/theses.shtml b/helm/www/matita/theses.shtml
new file mode 100644 (file)
index 0000000..37a2b41
--- /dev/null
+++ b/helm/www/matita/theses.shtml
@@ -0,0 +1,39 @@
+<!--
+<small>
+  <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
+</small>
+-->
+
+<ul>
+  
+  <li class="paper">
+  <a name="freescale"/>
+  <span class="paper_author">
+    Cosimo Arndt Oliboni
+  </span><br/>
+  <span class="paper_title">
+    Matita come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva
+    dei Microcontroller a 8 bit Freescale
+  </span>
+  <a class="paper_download" href="PAPERS/oliboni.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <span class="paper_info">
+    Undergraduate thesis, University of Bologna, 2008.
+  </span>
+  <span class="XXXpaper_abstract">
+   We describe an executable formalization of the operational semantics of
+   every microcontroller of the Freescale 8-bit families (HC05, HC08, HCS08,
+   RS08). The formalization is done in Matita and heavily relies on dependent
+   types (for static checking) and executable exhaustive tests (to avoid
+   under-specification and specification errors). Real world programs have
+   been compiled to assembly (using CodeWarrior) and executed both with
+   the emulator formalized in Matita and its extracted OCaml version (for
+   performance reasons). All aspects of memory management and execution are
+   captured, up to the point of precisely characterizing the number of clock
+   cycles required by any single instruction. The manuscript is in Italian
+   only.
+  </span>
+  </li>
+  
+</ul>