| 1 | \documentclass{llncs} |
|---|
| 2 | |
|---|
| 3 | \usepackage[english]{babel} |
|---|
| 4 | \usepackage[colorlinks]{hyperref} |
|---|
| 5 | |
|---|
| 6 | \title{Proving the correctness of an assembler for the MCS-51 microprocessor} |
|---|
| 7 | \author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen} |
|---|
| 8 | \institute{Dipartimento di Scienze dell'Informazione, Universit\'a di Bologna} |
|---|
| 9 | |
|---|
| 10 | \bibliographystyle{splncs03} |
|---|
| 11 | |
|---|
| 12 | \begin{document} |
|---|
| 13 | |
|---|
| 14 | \maketitle |
|---|
| 15 | |
|---|
| 16 | \begin{abstract} |
|---|
| 17 | \end{abstract} |
|---|
| 18 | |
|---|
| 19 | % ---------------------------------------------------------------------------- % |
|---|
| 20 | % SECTION % |
|---|
| 21 | % ---------------------------------------------------------------------------- % |
|---|
| 22 | \section{Introduction} |
|---|
| 23 | \label{sect.introduction} |
|---|
| 24 | |
|---|
| 25 | This paper discusses the proof of correctness of an assembler for the Intel MCS-51 8-bit family of microprocessors. |
|---|
| 26 | |
|---|
| 27 | The work presented herein is a component of the EU-funded CerCo (`Certified Complexity') project. |
|---|
| 28 | CerCo aims to produce a verified compiler from a large subset of C to the machine language of a microprocessor commonly used in embedded systems. |
|---|
| 29 | In this respect, CerCo aims to go beyond the state of the art in verified compiler technology. |
|---|
| 30 | |
|---|
| 31 | Arguably, the CompCert C compiler currently represents the state of the art in the field of verified compilers. |
|---|
| 32 | However, the verified backend of the CompCert C compiler stops at Power PC and ARM assembly \emph{languages}. |
|---|
| 33 | Assembly of these languages into machine code is left untrusted. |
|---|
| 34 | We aim to go further. |
|---|
| 35 | |
|---|
| 36 | The MCS-51 is CerCo's target processor. |
|---|
| 37 | |
|---|
| 38 | % ---------------------------------------------------------------------------- % |
|---|
| 39 | % SECTION % |
|---|
| 40 | % ---------------------------------------------------------------------------- % |
|---|
| 41 | \subsection{CerCo} |
|---|
| 42 | \label{subsect.cerco} |
|---|
| 43 | |
|---|
| 44 | % ---------------------------------------------------------------------------- % |
|---|
| 45 | % SECTION % |
|---|
| 46 | % ---------------------------------------------------------------------------- % |
|---|
| 47 | \subsection{Overview of the paper} |
|---|
| 48 | \label{subsect.overview.of.the.paper} |
|---|
| 49 | |
|---|
| 50 | % ---------------------------------------------------------------------------- % |
|---|
| 51 | % SECTION % |
|---|
| 52 | % ---------------------------------------------------------------------------- % |
|---|
| 53 | \section{The proof} |
|---|
| 54 | \label{sect.the.proof} |
|---|
| 55 | |
|---|
| 56 | % ---------------------------------------------------------------------------- % |
|---|
| 57 | % SECTION % |
|---|
| 58 | % ---------------------------------------------------------------------------- % |
|---|
| 59 | \subsection{Matita} |
|---|
| 60 | \label{subsect.matita} |
|---|
| 61 | |
|---|
| 62 | % ---------------------------------------------------------------------------- % |
|---|
| 63 | % SECTION % |
|---|
| 64 | % ---------------------------------------------------------------------------- % |
|---|
| 65 | \section{Conclusions} |
|---|
| 66 | \label{sect.conclusions} |
|---|
| 67 | |
|---|
| 68 | \bibliography{cpp-2011.bib} |
|---|
| 69 | |
|---|
| 70 | \end{document} |
|---|
