source: src/ASM/CPP2011/cpp-2011.tex @ 927

Last change on this file since 927 was 927, checked in by mulligan, 8 years ago

changes

File size: 3.0 KB
Line 
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
25This paper discusses the proof of correctness of an assembler for the Intel MCS-51 8-bit family of microprocessors.
26
27The work presented herein is a component of the EU-funded CerCo (`Certified Complexity') project.
28CerCo aims to produce a verified compiler from a large subset of C to the machine language of a microprocessor commonly used in embedded systems.
29In this respect, CerCo aims to go beyond the state of the art in verified compiler technology.
30
31Arguably, the CompCert C compiler currently represents the state of the art in the field of verified compilers.
32However, the verified backend of the CompCert C compiler stops at Power PC and ARM assembly \emph{languages}.
33Assembly of these languages into machine code is left untrusted.
34We aim to go further.
35
36The 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}
Note: See TracBrowser for help on using the repository browser.