Changeset 2088


Ignore:
Timestamp:
Jun 15, 2012, 11:52:37 AM (5 years ago)
Author:
mulligan
Message:

Added list of keywords as is required. Other minor changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-asm/cpp-2012-asm.tex

    r2087 r2088  
    3535                        \[\fbox{\TheSbox}\]}
    3636
    37 \title{On the correctness of an optimising assembler for the Intel MCS-51 microprocessor\thanks{The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881}}
     37\title{On the correctness of an optimising assembler for the Intel MCS-51 microprocessor\thanks{The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881.}}
    3838\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
    3939\institute{Dipartimento di Scienze dell'Informazione,\\ Universit\'a di Bologna}
     
    5858Our strategy offers increased flexibility over the traditional approach to proving the correctness of assemblers, wherein addresses in assembly are kept opaque and immutable.
    5959In particular, we may experiment with allowing the benign manipulation of addresses.
     60\keywords{Verified software, CerCo (Certified Complexity), MCS-51 microcontroller, Matita proof assistant}
    6061\end{abstract}
    6162
Note: See TracChangeset for help on using the changeset viewer.