source: Papers/cerco-assembler-2012/cerco-assembler.tex @ 3615

\documentclass[a4paper, 10pt]{article}

\author{Jaap Boender and Dominic P. Mulligan and Claudio Sacerdoti Coen}
\title{On the correctness of an optimising assembler for the MCS-51 microprocessor}
\date{\today}

\begin{document}

\maketitle

\begin{abstract}
\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Section
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
\label{sect.introduction}

This paper describes the formalisation and proof of correctness of an optimising assembler for the MCS-51 microprocessor.
The formalisation and proof of correctness have been carried out in the Matita proof assistant, a dependently-typed, tactic driven system similar to Coq.
The complete formalisation of the microprocessor and assembler forms a substantial and important component of the EU's CerCo (`Certified Complexity') project.

The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s.
Despite its relative age, the microprocessor is still manufactured in quantity by numerous foundries and is a popular component in embedded devices, where simple, well-tested and inexpensive microprocessors find their niche.
Further, the processor has been used as the basis for numerous derivatives over the last three decades.
However, compared to its more modern brethren the MCS-51 has a paucity of features: most MCS-51 derivatives do not feature any instruction caching, pipelining of instructions, branch prediction or features typical of cutting-edge microprocessors.

The MCS-51's simplicity means it is well suited for CerCo's ends.
CerCo aims to construct and prove correct a concrete cost preserving compiler for a large subset of the C programming language.
The main novelty of the CerCo compiler is its certified lifting of a precise cost model.
This cost model is presented to the programmer as a series of \emph{cost annotations} that decorate the C source.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Section
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Overview of the paper}
\label{subsect.overview.paper}

\end{document}