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

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