source: src/ASM/SEFM2012/main.tex @ 1889

Last change on this file since 1889 was 1889, checked in by boender, 8 years ago
  • some pages of article
  • Property svn:executable set to *
File size: 1.1 KB
Line 
1\documentclass[a4paper]{llncs}
2\usepackage{alltt}
3\usepackage[utf8]{inputenc}
4
5\begin{document}
6
7\mainmatter
8\title{On the correctness of a branch displacement algorithm}
9\author{Jaap Boender \and Claudio Sacerdoti Coen}
10\institute{Alma Mater Studiorum---Università degli Studi di Bologna}
11
12\maketitle
13
14\begin{abstract}
15The branch displacement problem is a well-known problem in assembler design.
16It revolves around the feature, present in several processor families, of
17having different instructions, of different sizes, for jumps of different
18displacements. The problem, which is provably NP-hard, is then to select the
19instructions such that one ends up with the smallest possible program.
20
21During our research with the CerCo project on formally verifying a C compiler,
22we have implemented and proven correct an algorithm for this problem. In this
23paper, we discuss the problem, possible solutions, our specific solutions and
24the proofs.
25
26\keywords{formal verification, assembler, branch displacement optimisation}
27\end{abstract}
28
29\input{problem}
30\input{algorithm}
31
32\bibliography{biblio}
33\bibliographystyle{plain}
34
35\end{document}
Note: See TracBrowser for help on using the repository browser.