# source:Papers/sttt/main.tex@3470

Last change on this file since 3470 was 3470, checked in by boender, 6 years ago
• added first version of STTT paper
• Property svn:executable set to *
File size: 1.6 KB
Line
1\documentclass[twocolumn,draft]{svjour3}
2\usepackage{algpseudocode}
3%\usepackage{algorithmicx}
4\usepackage{alltt}
5\usepackage{amsfonts}
6\usepackage{amsmath}
7\usepackage[british]{babel}
8\usepackage{caption}
9\usepackage{hyperref}
10\usepackage[utf8]{inputenc}
11\usepackage{listings}
12\usepackage{subcaption}
13
14\renewcommand{\verb}{\lstinline}
15\def\lstlanguagefiles{lst-grafite.tex}
16\lstset{language=Grafite}
17
18\begin{document}
19
20\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}}
21\author{Jaap Boender \and Dominic Mulligan \and Claudio Sacerdoti Coen}
22
23\maketitle
24
25\begin{abstract}
26The branch displacement problem is a well-known problem in assembler design.
27It revolves around the feature, present in several processor families, of
28having different instructions, of different sizes, for jumps of different
29displacements. The problem, which is provably NP-hard, is then to select the
30instructions such that one ends up with the smallest possible program.
31
32During our research with the CerCo project on formally verifying a C compiler,
33we have implemented and proven correct an algorithm for this problem. In this
34paper, we discuss the problem, possible solutions, our specific solutions and
35the proofs.
36
37\keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation}
38\end{abstract}
39
40\input{problem}
41\input{algorithm}
42\input{proof}
43\input{conclusion}
44
45\bibliography{biblio}
46\bibliographystyle{spbasic}
47
48\end{document}
Note: See TracBrowser for help on using the repository browser.