source: Deliverables/D6.2/addendum.tex @ 3285

% CerCo: Certified Complexity
%
% Addendum to Deliverable 6.2
%
% Plan for Dissemination and Use
% Addendum requested by project reviewers at end of year 1.
%
% Ian Stark
% 2011-05

\documentclass[11pt,a4paper]{article}
\usepackage{../style/cerco}

\hypersetup{bookmarksopenlevel=2}

\title{
INFORMATION AND COMMUNICATION TECHNOLOGIES\\
(ICT)\\
PROGRAMME\\
\vspace*{1cm}Project FP7-ICT-2009-C-243881 {\cerco}}

\date{ }
\author{}

\begin{document}
\thispagestyle{empty}

\vspace*{-1cm}
\begin{center}
\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
\end{center}

\begin{minipage}{\textwidth}
\maketitle
\end{minipage}


\vspace*{0.5cm}
\begin{center}
\begin{LARGE}
\bf
Addendum to Deliverable 6.2\\[\jot]
Future Dissemination Plans
\end{LARGE} 
\end{center}

\vspace*{2cm}
\begin{center}
\begin{large}
Version 1.0
\end{large}
\end{center}

\vspace*{0.5cm}
\begin{center}
\begin{large}
Main Authors:\\
I. Stark
\end{large}
\end{center}

\vspace*{\fill}
\noindent
Project Acronym: {\cerco}\\
Project full title: Certified Complexity\\
Proposal/Contract no.: FP7-ICT-2009-C-243881 {\cerco}\\

\clearpage \pagestyle{myheadings} \markright{{\cerco}, FP7-ICT-2009-C-243881}

\tableofcontents

\section{Premise}
Deliverable~6.2, the \emph{Plan for the Use and Dissemination of Foreground}
was submitted as the first report of the {\cerco} project.  Following the
scientific review of the project at the end of its first year, the reviewers
recommended preparation of an addendum to specifically list future
dissemination plans.  This is that addendum.


\section{Dissemination Plans}

The {\cerco} project represents an unprecedented effort to create a
machine-verified chain of trust for analysing program performance properties
through compilation.  This combines novel work in the theory of machine proof
and certified compilation with its concrete application to a specific
industrial microcontroller.

As appropriate for a project in the \emph{Future and Emerging Technologies}
programme, a major target for dissemination is to influence future work by
other European research groups, through a direct demonstration of a verified
resource-aware compiler.  The immediate routes for this are the standard ones
for academic communication and training: conference papers, journal articles,
collaborative workshops, tutorial events.  In addition, with the project
centred around a substantial implementation effort, the compiler code and the
machine proofs are themselves vehicles for dissemination to other researchers.

The longer-term dissemination targets are the potential end-users of verified
compiler technology: programmers of commodity microcontrollers being used in
tightly resource-constrained embedded applications --- particularly those
where safety-critical requirements mandate a high quality of performance
certification.  Possible routes for this long-term dissemination are through
research symposia at industrially-relevant conferences, and tutorial sessions
at conferences or other events with significant industrial presence.

\subsection{Conferences and Workshops}

We propose to submit results of {\cerco} research for presentation at
appropriate international venues.  There are very many conferences dealing
with {\cerco}-related areas: compilation technology, machine-assisted proof,
resource analysis, etc.  For example, the following are particularly close to
{\cerco} activity:
\begin{itemize}
\item CPP: Certified Programs and Proofs
\item FMCAD: Formal Methods in Computer-Aided Design
\item LOLA: Syntax and Semantics of Low-Level Languages
\item VSTTE: Verified Software: Theories, Tools and Experiments
\item SSV: Systems Software Verification
\item FORMATS: Formal Modeling and Analysis of Timed Systems
\item ITP: Interactive Theorem Proving (was TPHOLs)
\item PSI: Program Understanding
\end{itemize} 
Beyond these, there are many high-quality general conferences which would also
provide a good venue for publicising the results of the project.  For example:
\begin{itemize}
\item POPL: Principles of Programming Languages
\item LPAR: Logic for Programming, Artificial Intelligence and Reasoning
\item CC: Compiler Construction
\item FM: International Symposium on Formal Methods
\item APLAS: Asian Symposium on Programming Languages and Reasoning
\end{itemize}
In addition to these subject-related events, {\cerco} will contribute to
FET-organized activities, such as conferences, dedicated workshops, working
groups and other meetings.

 
\subsection{Journals}

The project participants will publish papers and articles based on {\cerco}
results in appropriate archival venues, throughout the duration of the
project.  Most of the conferences listed above have formal proceedings;
several also have affiliated special issues in journals, for publishing
extended versions of papers.  In addition, we expect to submit free-standing
articles to appropriate journals, such as:
\begin{itemize}
\item Journal of Automated Reasoning
\item Journal of Formalized Reasoning
\item Information and Computation
\item Theoretical Computer Science
\item Higher-Order and Symbolic Computation
\item Communications of the ACM
\item Science of Computer Programming
\end{itemize}

\subsection{Tutorials and Training}

As established researchers, the project participants will give lectures and
tutorials on {\cerco}-related research as part of their existing dissemination
activity throughout the course of the project.  However, in addition to this
{\cerco} will organise specific training activities targeted at the scientific
community, and at potential industrial stakeholders.  These are formal
deliverables of Work Package~6 in the project contract.  To increase
visibility, and promote attendance, we would affiliate any event with an
existing conference or school.  For example, a {\cerco} tutorial would much
more effectively reach a suitable audience if given as part of an established
summer school.  It may also be appropriate to collaborate with related EU
projects or research groups in management of such events.

To benefit the most from {\cerco} project results, such events should take
place in the final year of the project.  We plan to identify appropriate
venues during the second year of {\cerco}.

\subsection{Artefacts}

A significant part of {\cerco} is the implementation effort, with accompanying
experience gained in developing and verifying a machine-checked resource-aware
compiler.  This gives rise to specific software artefacts, which other
projects can learn from and build upon.  All these will be made
publically-available at project milestones, and form a notable route for
dissemination of the project outcomes.  The full report D6.2 describes in
detail the target communities and potential users of this software; here we
summarize.

\subsubsection{Untrusted Cost-Annotating Compiler}

This is a functional compiler from C to assembler, structured and instrumented
to trace the evolution of high-level code fragments to low-level instruction
sequences and match their execution costs.

\subsubsection{Untrusted Compiler within Proof-Assistant}

This will be an implementation of the CerCo cost-annotating compiler within
the \emph{Matita} proof assistant.  This takes the form of a formal
specification of the compiler in the calculus of (co)inductive constructions,
arranged in so as to be directly executable within \emph{Matita}.  

\subsubsection{Trusted Cost-Annotating Compiler}

This is the final product of the {\cerco} project and brings together a number
of distinct elements:
\begin{itemize}
\item An executable compiler which automatically annotates C source code with
  machine execution costs;
\item A machine-certified proof that the compiler is functionally correct and
  that the automatic annotations exactly reflect low-level instruction costs;
\item Extensions to the \emph{Matita} interactive proof engine to automate
  this substantial proof;
\item Example integration of these low-level cost-annotations with high-level
  program analysis tools in the \emph{Frama-C} framework.
\end{itemize}


\end{document}

% LocalWords:  Sacerdoti Coen microcontroller FMCAD VSTTE TPHOLs LPAR Artefacts