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} |
---|