Changeset 3472 for Papers


Ignore:
Timestamp:
Sep 11, 2014, 12:24:34 PM (5 years ago)
Author:
mulligan
Message:

title and abstract changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/sttt/main.tex

    r3471 r3472  
    1818\begin{document}
    1919
    20 \title{On the correctness of a branch displacement algorithm
     20\title{A verified optimising assembler
    2121\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}}
    2222\author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
     23\institute{Department of Computer Science, University of Middlesex \and Computer Laboratory, University of Cambridge \and Dipartimento di Informatica, University of Bologna}
    2324
    2425\maketitle
     
    2930
    3031As 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.
    31 Our assembler targets the instruction set of a typical micro-controller, the \textsc{mcs}-51.
    32 As 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.
    33 Out of necessity, then, our assembler must implement an algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct.
     32Our assembler targets the instruction set of a typical micro-controller, the Intel \textsc{mcs}-51 series.
     33As is common in embedded systems development, this micro-controller has a paucity of available code memory and therefore we face an additional pressure in reducing the size of any assembled machine code program.
     34Out of necessity, then, our assembler implements an algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct.
    3435
    3536We 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.
Note: See TracChangeset for help on using the changeset viewer.