# source:src/ASM/CPP2012-policy/main.tex@2064

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