helm/www/matita1.0/theses.shtml

   1 <!--
   2 <small>
   3   <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
   4 </small>
   5 -->
   6
   7 <ul>
   8
   9   <li class="paper">
  10   <a name="freescale"/>
  11   <span class="paper_author">
  12     Cosimo Arndt Oliboni
  13   </span><br/>
  14   <span class="paper_title">
  15     Matita come Supporto per Specifiche Eseguibili: Formalizzazione Interattiva
  16     dei Microcontroller a 8 bit Freescale
  17   </span>
  18   <a class="paper_download" href="PAPERS/oliboni.pdf">
  19     <span class="pdf_logo">.pdf</span>
  20   </a>
  21   <span class="paper_info">
  22     Undergraduate thesis, University of Bologna, 2008.
  23   </span>
  24   <span class="XXXpaper_abstract">
  25    We describe an executable formalization of the operational semantics of
  26    every microcontroller of the Freescale 8-bit families (HC05, HC08, HCS08,
  27    RS08). The formalization is done in Matita and heavily relies on dependent
  28    types (for static checking) and executable exhaustive tests (to avoid
  29    under-specification and specification errors). Real world programs have
  30    been compiled to assembly (using CodeWarrior) and executed both with
  31    the emulator formalized in Matita and its extracted OCaml version (for
  32    performance reasons). All aspects of memory management and execution are
  33    captured, up to the point of precisely characterizing the number of clock
  34    cycles required by any single instruction. The manuscript is in Italian
  35    only.
  36   </span>
  37   </li>
  38
  39 </ul>