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

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