Changeset 3472
 Timestamp:
 Sep 11, 2014, 12:24:34 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/sttt/main.tex
r3471 r3472 18 18 \begin{document} 19 19 20 \title{ On the correctness of a branch displacement algorithm20 \title{A verified optimising assembler 21 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 FETOpen grant number 243881}} 22 22 \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} 23 24 24 25 \maketitle … … 29 30 30 31 As 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 languagewe have implemented and proved correct an assembler within an interactive theorem prover. 31 Our assembler targets the instruction set of a typical microcontroller, the \textsc{mcs}51.32 As is common in embedded systems , this microcontroller has a paucity of available code memory and therefore we faceadditional pressure in reducing the size of any assembled machine code program.33 Out of necessity, then, our assembler must implementan algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct.32 Our assembler targets the instruction set of a typical microcontroller, the Intel \textsc{mcs}51 series. 33 As is common in embedded systems development, this microcontroller has a paucity of available code memory and therefore we face an additional pressure in reducing the size of any assembled machine code program. 34 Out of necessity, then, our assembler implements an algorithm for solving the branch displacement problem, and we must prove that this algorithm is correct. 34 35 35 36 We 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.