Changeset 549 for Deliverables

Timestamp:

Feb 17, 2011, 11:46:40 AM (11 years ago)

Author:

mulligan

Message:

Half of bibliography added.

Location:

Deliverables/D4.1/ITP-Paper

Files:

• itp-2011.bib (added)
• itp-2011.tex (modified) (7 diffs)

Deliverables/D4.1/ITP-Paper/itp-2011.tex

@@ -58 +58 @@
 \institute{Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna}
 
+\bibliographystyle{alpha}
+
 \begin{document}
 
@@ -651 +653 @@
 These traces were useful in spotting anything that was `obviously' wrong with the execution of the program.
 
-Further, we made use of an open source emulator for the MCS-51, \texttt{mcu8051ide}.
-Using our execution traces, we were able to step through a compiled program, one instruction at a time, in \texttt{mcu8051ide}, and compare the resulting execution trace with the trace produced by our emulator.
+Further, we used MCU 8051 IDE as a reference.
+Using our execution traces, we were able to step through a compiled program, one instruction at a time, in MCU 8051 IDE, and compare the resulting execution trace with the trace produced by our emulator.
 
 Our Matita formalisation was largely copied from the O'Caml source code, apart from changes related to addressing modes already mentioned.
@@ -668 +670 @@
 Moreover, in addition to formalising the interface of an MCS-51 processor, we have also built a complete MCS-51 ecosystem: the UART, the I/O lines, and hardware timers, along with an assembler.
 
-Similar work to ours can be found in~\cite{A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture Anthony Fox and Magnus O. Myreen}.
+Similar work to ours can be found in~\cite{fox:trustworthy:2010}.
 Here, the authors describe the formalisation, in HOL4, of the ARMv7 instruction set architecture, and point to a good list of references to related work in the literature.
 This formalisation also considers the machine code level, as opposed to only considering an abstract assembly language.
@@ -674 +676 @@
 However, we go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction to machine code.
 
-Further, in~\cite{again} the authors validated their formalisation by using development boards and random testing.
+Further, in~\cite{fox:trustworthy:2010} the authors validated their formalisation by using development boards and random testing.
 However, we currently rely on non-exhaustive testing against a third party emulator.
 We leave similar exhaustive testing for future work.
 
-Executability is another key difference between our work and~\cite{again}.
-In~\cite{again} the authors provide an automation layer to derive single step theorems: if the processor is in a particular state that satisfies some preconditions, then after execution of an instruction it will reside in another state satisfying some postconditions.
+Executability is another key difference between our work and~\cite{fox:trustworthy:2010}.
+In~\cite{fox:trustworthy:2010} the authors provide an automation layer to derive single step theorems: if the processor is in a particular state that satisfies some preconditions, then after execution of an instruction it will reside in another state satisfying some postconditions.
 We do not need single step theorems of this form.
 This is because Matita is based on a logic that internalizes conversion.
@@ -687 +689 @@
 In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably.
 
-Perhaps the closest project to CerCo is CompCert~\cite{compcert}.
+Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009,blazy:formal:2006}.
 CompCert concerns the certification of an ARM compiler and includes a formalisation in Coq of a subset of ARM.
 Coq and Matita essentially share the same logic.
@@ -698 +700 @@
 Even from a technical level the two formalisations differ: while we tried to exploit dependent types as often as possible, CompCert largely sticks to the non-dependent fragment of Coq.
 
-In~\cite{Robert Atkey. CoqJVM: An executable specification of the Java virtual machine using dependent types. In Marino Miculan, Ivan Scagnetto, and Furio Honsell, editors, TYPES, volume 4941 of Lecture Notes in Computer Science, pages 18-32.  Springer, 2007.} Atkey presents an executable specification of the Java virtual machine which uses dependent types.
+In~\cite{atkey:coqjvm:2007} Atkey presents an executable specification of the Java virtual machine which uses dependent types.
 As we do, dependent types are used to remove spurious partiality from the model, and to lower the need for over-specifying the behaviour of the processor in impossible cases.
 Our use of dependent types will also help to maintain invariants when we prove the correctness of the CerCo prototype compiler.
 
-Finally, in~\cite{Susmit Sarkar, Pater Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant Magnus O. Myreen, and Jade Alglave. The semantics of x86-CC multiprocessor machine code. In Principles of Programming Languages (POPL). ACM, 2009.} Sarkar et al provide an executable semantics for x86-CC multiprocessor machine code.
+Finally, in~\cite{sarkar:semantics:2009} Sarkar et al provide an executable semantics for x86-CC multiprocessor machine code.
 This machine code exhibits a high degree of non-uniformity similar to the MCS-51.
 However, only a very small subset of the instruction set is considered, and they over-approximate the possibilities of unorthogonality of the instruction set, largely dodging the problems we had to face.
@@ -728 +730 @@
 - WE FORMALIZE ALSO I/O ETC. NOT ONLY THE INSTRUCTION SELECTION (??)
   How to test it? Specify it?
+
+\bibliography{itp-2011.bib}
 
 \newpage