# Changeset 512 for Deliverables/D4.1/ITP-Paper/itp-2011.tex

Ignore:
Timestamp:
Feb 15, 2011, 10:39:42 AM (9 years ago)
Message:

tidy up of the intro

File:
1 edited

Unmodified
Removed
• ## Deliverables/D4.1/ITP-Paper/itp-2011.tex

 r511 \usepackage[utf8x]{inputenc} \usepackage{listings} \usepackage{mdwlist} \usepackage{microtype} \usepackage{stmaryrd} \label{sect.introduction} Formal methods are aimed at increasing our confidence in our software and hardware artifacts. Ideally, in the future we would like all artifacts to be equipped with a formal specification and a proof of correctness of the implementation. Nowadays practically all programs are written in high level languages and then compiled into low level ones. Thus the specifications are also given at high level and correctness is proved reasoning automatically or interactively on the source code. The code that is actually run, however, is the object code generated by the compiler. A few simple questions then arise: Formal methods are designed to increase our confidence in the design and implementation of software (and hardware). Ideally, we would like all software to come equipped with a formal specification, along with a proof of correctness for the implementation. Today practically all programs are written in high level languages and then compiled into low level ones. Specifications are therefore also given at a high level and correctness can be proved by reasoning automatically or interactively on the program's source code. The code that is actually run, however, is not the high level source code that we reason on, but the object code that is generated by the compiler. A few simple 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? Compiler verification, as of late, is a hot topic' in computer science research. So far, it has been focused on the first and last question only. In particular, the attention has been put only on extensional properties, which are easily preserved during compilation: it is sufficient to completely preserve the denotational semantics of the input program. \end{itemize*} These questions, and others like them, motivate a current hot topic' in computer science research: \emph{compiler verification}. So far, the field has been focused on the first and last questions only. In particular, much attention has been placed on verifying compiler correctness with respect to extensional properties of programs, which are easily preserved during compilation; it is sufficient to completely preserve the denotational semantics of the input program. The situation is definitely more complex when we also take in account
Note: See TracChangeset for help on using the changeset viewer.