Changeset 927 for src


Ignore:
Timestamp:
Jun 9, 2011, 5:06:35 PM (10 years ago)
Author:
mulligan
Message:

changes

Location:
src/ASM/CPP2011
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/CPP2011/cpp-2011.tex

    r918 r927  
    44\usepackage[colorlinks]{hyperref}
    55
    6 \title{Proving the correctness of an assembler for the MCS-51}
    7 \author{}
    8 \institute{Universit\'a di Bologna}
     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}
    911
    1012\begin{document}
    … …  
    2123\label{sect.introduction}
    2224
     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
    2370\end{document}
Note: See TracChangeset for help on using the changeset viewer.