- Timestamp:
- Jun 15, 2012, 11:52:37 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CPP2012-asm/cpp-2012-asm.tex
r2087 r2088 35 35 \[\fbox{\TheSbox}\]} 36 36 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.}} 38 38 \author{Dominic P. Mulligan \and Claudio Sacerdoti Coen} 39 39 \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. 59 59 In particular, we may experiment with allowing the benign manipulation of addresses. 60 \keywords{Verified software, CerCo (Certified Complexity), MCS-51 microcontroller, Matita proof assistant} 60 61 \end{abstract} 61 62
Note: See TracChangeset
for help on using the changeset viewer.