Last change
on this file since 2045 was
1889,
checked in by boender, 8 years ago



Property svn:executable set to
*

File size:
1.1 KB

Line  

1  \documentclass[a4paper]{llncs} 

2  \usepackage{alltt} 

3  \usepackage[utf8]{inputenc} 

4  

5  \begin{document} 

6  

7  \mainmatter 

8  \title{On the correctness of a branch displacement algorithm} 

9  \author{Jaap Boender \and Claudio Sacerdoti Coen} 

10  \institute{Alma Mater StudiorumUniversità degli Studi di Bologna} 

11  

12  \maketitle 

13  

14  \begin{abstract} 

15  The branch displacement problem is a wellknown problem in assembler design. 

16  It revolves around the feature, present in several processor families, of 

17  having different instructions, of different sizes, for jumps of different 

18  displacements. The problem, which is provably NPhard, is then to select the 

19  instructions such that one ends up with the smallest possible program. 

20  

21  During our research with the CerCo project on formally verifying a C compiler, 

22  we have implemented and proven correct an algorithm for this problem. In this 

23  paper, we discuss the problem, possible solutions, our specific solutions and 

24  the proofs. 

25  

26  \keywords{formal verification, assembler, branch displacement optimisation} 

27  \end{abstract} 

28  

29  \input{problem} 

30  \input{algorithm} 

31  

32  \bibliography{biblio} 

33  \bibliographystyle{plain} 

34  

35  \end{document} 

Note: See
TracBrowser
for help on using the repository browser.