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

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 | \mainmatter |
---|

21 | \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}} |
---|

22 | \author{Jaap Boender\inst{1} \and Claudio Sacerdoti Coen\inst{2}} |
---|

23 | \institute{Foundations of Computing Group\\Department of Computer Science\\School of Science and Technology\\Middlesex University, London, UK\\ |
---|

24 | \email{J.Boender@mdx.ac.uk} |
---|

25 | \and |
---|

26 | Dipartimento di Scienze dell'Informazione,\\ |
---|

27 | Universit\`a degli Studi di Bologna, Italy\\ |
---|

28 | \email{sacerdot@cs.unibo.it}} |
---|

29 | |
---|

30 | \maketitle |
---|

31 | |
---|

32 | \begin{abstract} |
---|

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

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

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

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

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

38 | |
---|

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

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

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

42 | the proofs. |
---|

43 | |
---|

44 | \keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation} |
---|

45 | \end{abstract} |
---|

46 | |
---|

47 | \input{problem} |
---|

48 | \input{algorithm} |
---|

49 | \input{proof} |
---|

50 | \input{conclusion} |
---|

51 | |
---|

52 | \bibliography{biblio} |
---|

53 | \bibliographystyle{splncs03} |
---|

54 | |
---|

55 | \end{document} |
---|