[1889] | 1 | \documentclass[a4paper]{llncs} |
---|

[2054] | 2 | \usepackage{algpseudocode} |
---|

[1889] | 3 | \usepackage{alltt} |
---|

[2054] | 4 | \usepackage{amsfonts} |
---|

[2064] | 5 | \usepackage[british]{babel} |
---|

[2084] | 6 | \usepackage{hyperref} |
---|

[1889] | 7 | \usepackage[utf8]{inputenc} |
---|

[2064] | 8 | \usepackage{listings} |
---|

[1889] | 9 | |
---|

[2064] | 10 | \renewcommand{\verb}{\lstinline} |
---|

| 11 | \def\lstlanguagefiles{lst-grafite.tex} |
---|

| 12 | \lstset{language=Grafite} |
---|

| 13 | |
---|

[1889] | 14 | \begin{document} |
---|

| 15 | |
---|

| 16 | \mainmatter |
---|

[2084] | 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}} |
---|

[1889] | 18 | \author{Jaap Boender \and Claudio Sacerdoti Coen} |
---|

[2084] | 19 | \institute{Dipartimento di Scienze dell'Informazione, Università degli Studi di Bologna} |
---|

[1889] | 20 | |
---|

| 21 | \maketitle |
---|

| 22 | |
---|

| 23 | \begin{abstract} |
---|

| 24 | The branch displacement problem is a well-known problem in assembler design. |
---|

| 25 | It revolves around the feature, present in several processor families, of |
---|

| 26 | having different instructions, of different sizes, for jumps of different |
---|

| 27 | displacements. The problem, which is provably NP-hard, is then to select the |
---|

| 28 | instructions such that one ends up with the smallest possible program. |
---|

| 29 | |
---|

| 30 | During our research with the CerCo project on formally verifying a C compiler, |
---|

| 31 | we have implemented and proven correct an algorithm for this problem. In this |
---|

| 32 | paper, we discuss the problem, possible solutions, our specific solutions and |
---|

| 33 | the proofs. |
---|

| 34 | |
---|

| 35 | \keywords{formal verification, assembler, branch displacement optimisation} |
---|

| 36 | \end{abstract} |
---|

| 37 | |
---|

| 38 | \input{problem} |
---|

| 39 | \input{algorithm} |
---|

[2064] | 40 | \input{proof} |
---|

| 41 | \input{conclusion} |
---|

[1889] | 42 | |
---|

| 43 | \bibliography{biblio} |
---|

[2084] | 44 | \bibliographystyle{splncs03} |
---|

[1889] | 45 | |
---|

| 46 | \end{document} |
---|