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

Last change on this file since 3346 was 3342, checked in by boender, 6 years ago
  • completed reworking of proofs
  • Property svn:executable set to *
File size: 1.9 KB
RevLine 
[3304]1\documentclass[a4paper]{llncs}
2\usepackage{algpseudocode}
[3342]3%\usepackage{algorithmicx}
[3304]4\usepackage{alltt}
5\usepackage{amsfonts}
[3338]6\usepackage{amsmath}
[3304]7\usepackage[british]{babel}
8\usepackage{hyperref}
9\usepackage[utf8]{inputenc}
10\usepackage{listings}
11
12\renewcommand{\verb}{\lstinline}
13\def\lstlanguagefiles{lst-grafite.tex}
14\lstset{language=Grafite}
15
16\begin{document}
17
18\mainmatter
19\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}}
20\author{Jaap Boender\inst{1} \and Claudio Sacerdoti Coen\inst{2}}
21\institute{Foundations of Computing Group\\Department of Computer Science\\School of Science and Technology\\Middlesex University, London, UK\\
22\email{J.Boender@mdx.ac.uk}
23\and
24Dipartimento di Scienze dell'Informazione,\\
25Universit\`a degli Studi di Bologna, Italy\\
26\email{sacerdot@cs.unibo.it}}
27
28\maketitle
29
30\begin{abstract}
31The branch displacement problem is a well-known problem in assembler design.
32It revolves around the feature, present in several processor families, of
33having different instructions, of different sizes, for jumps of different
34displacements. The problem, which is provably NP-hard, is then to select the
35instructions such that one ends up with the smallest possible program.
36
37During our research with the CerCo project on formally verifying a C compiler,
38we have implemented and proven correct an algorithm for this problem. In this
39paper, we discuss the problem, possible solutions, our specific solutions and
40the proofs.
41
[3342]42\keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation}
[3304]43\end{abstract}
44
45\input{problem}
46\input{algorithm}
47\input{proof}
48\input{conclusion}
49
50\clearpage
51\bibliography{biblio}
52\bibliographystyle{splncs03}
53
54\end{document}
Note: See TracBrowser for help on using the repository browser.