]> matita.cs.unibo.it Git - helm.git/blob - helm/www/matita/theses.shtml
...
[helm.git] / helm / www / matita / 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>