Changeset 2088 for src

Timestamp:

Jun 15, 2012, 11:52:37 AM (9 years ago)

Author:

mulligan

Message:

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

File:

• src/ASM/CPP2012-asm/cpp-2012-asm.tex (modified) (2 diffs)

src/ASM/CPP2012-asm/cpp-2012-asm.tex

@@ -35 +35 @@
                         \[\fbox{\TheSbox}\]}
 
-\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}}
+\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.}}
 \author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
 \institute{Dipartimento di Scienze dell'Informazione,\\ Universit\'a di Bologna}
@@ -58 +58 @@
 Our strategy offers increased flexibility over the traditional approach to proving the correctness of assemblers, wherein addresses in assembly are kept opaque and immutable.
 In particular, we may experiment with allowing the benign manipulation of addresses.
+\keywords{Verified software, CerCo (Certified Complexity), MCS-51 microcontroller, Matita proof assistant}
 \end{abstract}