source: Papers/sttt/main.tex @ 3471

Last change on this file since 3471 was 3471, checked in by mulligan, 6 years ago

reworked the abstract

  • Property svn:executable set to *
File size: 2.4 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
21\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 \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
23
24\maketitle
25
26\begin{abstract}
27Optimising assemblers face the `branch displacement problem', i.e. how best to choose between concrete machine code jump instructions---typically of differing instruction and offset sizes---when expanding pseudo-instructions.
28Ideally, a well-implemented optimising assembler would choose the set of jump expansions that minimises the size of the resulting machine code program, a task that is provably \textsc{np}-hard.
29
30As part of CerCo (`Certified Complexity')---an \textsc{eu}-funded project to develop a verified concrete complexity preserving compiler for a large subset of the C programming language---we have implemented and proved correct an assembler within an interactive theorem prover.
31Our assembler targets the instruction set of a typical micro-controller, the \textsc{mcs}-51.
32As is common in embedded systems, this micro-controller has a paucity of available code memory and therefore we face additional pressure in reducing the size of any assembled machine code program.
33Out of necessity, then, our assembler must implement an algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct.
34
35We discuss wider problems associated with proving an optimising assembler correct, discuss possible solutions to those problems, and detail our chosen solutions and their proofs of correctness.
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.