# Changeset 1205

Ignore:
Timestamp:
Sep 10, 2011, 12:16:54 PM (9 years ago)
Message:

typographical changes

File:
1 edited

### Legend:

Unmodified
 r1204 \author{Dominic P. Mulligan \and Claudio Sacerdoti Coen} \authorrunning{D. P. Mulligan \and C. Sacerdoti Coen} \institute{\vspace{-2em}} % \institute{Dipartimento di Scienze dell'Informazione,\\ Universit\a di Bologna} \institute{Dipartimento di Scienze dell'Informazione,\\ Universit\a di Bologna} \bibliographystyle{plain} The code that is actually run is not the high level source code that we reason on, but low level code generated by the compiler. Questions now arise:  What properties are preserved during compilation? Questions now arise: \begin{itemize*} \item What properties are preserved during compilation? \item What properties are affected by the compilation strategy? \item To what extent can you trust your compiler in preserving those properties? \end{itemize*} These and other questions motivate a current `hot topic' in computer science research: \emph{compiler verification} (e.g.~\cite{chlipala:verified:2010,leroy:formal:2009}, and so on). So far, the field has only been focused on the first and last questions.