source: Deliverables/D6.2/report.tex @ 23

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

\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
Report n. D6.2\\
Plan for the Use and dissemination of foreground\\
\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:\\
C. Sacerdoti Coen
\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}
The deliverable D6.2 \emph{Plan for the Use and dissemination of foreground}
is the first \textbf{report} of the \cerco{} project. The deliverable is
\textbf{confidential} and required an effort of about \textbf{2 person-months}.
The description of the deliverable in the Grant Agreement is the following one:
\begin{quote}
Plan for the Use and dissemination of foreground: An articulated dissemination plan, containing the individuation of the main target communities, and the relative exploitation strategies. 
\end{quote}

%{\textbf
%COMMISSION REQUIREMENTS:
%The plan is divided into two sections: one related to results that shall be disseminated and dissemination activities, including scientific publications   1  ; and one that describes exploitable results and related activities, which remain confidential, at least until the protection and the economic exploitation of the results have been implemented. The plan also describes the socio-economic impact of the results, the target group(s) for dissemination and exploitation activities, any contributions to standards or policy developments and any potential risk associated with the results.
%
%Dissemination activities include publications, websites, workshops, conferences, etc. This section shall summarise how participants plan to reach their target public, their communication strategy and a specific set of actions. Dissemination activities shall be presented in a verifiable way that will enable the Commission to keep track of them. Regarding scientific publications, references such as the title, the author, the scientific revue and the date of publication shall be provided. In addition to the information included in the report, participants shall provide these references, along with an abstract, to the Commission, at most two months after each scientific publication.
%
%3. Exploitable results
%
%This section is confidential. Participants shall first provide a list of all intellectual property rights that have been applied for or registered. Once again, such entries shall be verifiable; for instance, if a European patent has been applied for, the plan shall indicate the patent filing reference number.
%
%Participants shall also provide a list of all the results that may have commercial or industrial applications. Such results may include software, inventions, prototypes, compiled information and data, etc. The plan shall indicate the owner of each particular element of foreground, whether it is a single participant or several of them (in a situation of joint ownership). It shall briefly explain how the foreground has been or is going to be used, in either further research or commercial exploitation activities, including elements such as the following:
%
%    * Purpose, main features and benefits of each technology or product, derived from the research results: innovative aspects in comparison with technologies and products already available, needs for further R\&D activity (and implied risks), collaboration needs for exploitation (technology transfer activities);
%
%    * Customer detection: identification of the potential customers and the factors that affect their purchasing decisions;
%
%    * Features of the target market: size, growth rate, share that the technology/product could reach, driving factors likely to change the market, legal, technical and commercial barriers, other technologies likely to emerge in the near future;
%
%    * Positioning: how the participant (or other entity) entitled to the technology exploitation is positioned (or should be positioned) in the market, competing businesses/applications/technologies.
%
%The members of a consortium shall of course discuss these issues in advance and agree on the best strategy for the exploitation of foreground among the various existing options: direct or indirect exploitation, involving the whole consortium or only some of its members, exploitation through a separate legal entity such as a spin-off, etc.
%}

\section{Overview and General Approach}
\subsection{Overview of expected results}
Driven by a growing confidence in formal methods in general and interactive
theorem proving in particular, critical IT systems are slowly undergoing a
paradigm shift: testing of critical properties is going to be partially
replaced with formal verification on the programs written in an high level
language, and a set of formally verified tools (interpreters, compilers,
operating systems, communication libraries) is going to be used to grant preservation
of the verified property for the actual runs of the low level code.

The present state of the art already provides a few mildly optimizing
verified compilers that compete with traditional highly optimized compilers
and a few prototypes and experiments in the verification of operating systems.
However, the only properties that have been formalized are extensional, granting
that the high level semantics of the program --- usually specified in terms
of infinite resources (e.g. memory) --- is respected. All intensional
properties that have to do with resources are not currently preserved during
compilation or, at least, no formal proof of preservation is provided. Hence
high level programs still need to be extensively tested to verify resource
related properties like memory consumption or reaction time for reactive
and real time programs.

In \cerco{} we will address intentional properties of programs, in particular
execution time, and we will develop the first certified compiler that is able
to manifest in the source program some intentional properties, mainly
execution cost, that are inferred from the target program. The main issue
in doing so is to preserve compositionality of compilation: while the source
program undergoes several intentionally disruptive translations towards lower
and lower intermediate languages, we need to keep trace of the evolution of
sensible code fragments in order to relate source, intermediate and target
code fragments to back-propagate execution costs. Hence we expect to study
new more refined ways of expressing the operational semantics of programs
and to give a more refined notion of operational bisimulation, with the aim
of obtaining a characterization that is loose enough to capture some of the
most common and effective optimizations.

Once we can manifest in the source program execution costs computed on the
target program we will start the investigation of the exploitability of the
cost annotations. In particular, cost annotations must be combined with
extensional program invariants in order to obtain intensional program invariants
and be able to formally prove intensional properties of programs. We expect
this study to require a long effort and to be performed outside the project
timeframe. However, we assume that a combination of interactive theorem proving
and automatic formal methods (like abstract interpretation) will need to be
exploited and, in the project, we will focus on interactive theorem proving by
exploiting and providing basic tools to reason on cost invariants.

All the major deliverables of \cerco{} are prototypes --- either software
prototypes or formal certifications --- that are later integrated at project
milestones into major \cerco{} compiler snapshots. These snapshots are the
most appropriate deliverables for dissemination in the large and different
target communities are associated to the snapshots. We will discuss
the milestones and snapshots in details
in Section~\ref{byresult} in order to identify the potential target communities
and relative specific dissemination actions.


~\\

\begin{center}
\begin{tabular}{|lc|}
\hline
milestone name & due at month \\ \hline
Untrusted cost-annotating compiler & 12 \\
Untrusted CerCo compiler & 24 \\
Trusted CerCo compiler & 36 \\
\hline
\end{tabular}
\end{center}

~\\

\subsection{Academic exploitation}
 Academic partners will take great advantage from the results of CerCo mainly in terms of increased technical know-how and scientific knowledge, increased visibility in the scientific community of reference, increased expertise, exploitable for institutional academic purposes (e.g. didactic activities). We also expect that the rest of the academic community will take up the innovative ideas of the project, building on top of them code analyses at a level of accuracy that could have not been previously possible. Finally, we expect elaboration and instantiation of our methodology to other kinds of high level languages (functional, logic) and to more complex scenarios involving, for instance, a real time operating system.

\subsection{Industrial exploitation}
 The long term industrial exploitation of the results of the CerCo project is envisaged mainly in the area of the embedded systems/software, in particular in the case of safety critical applications and time critical (realtime) applications. In the short term, software houses producing compilers for embedded systems could immediately benefit from the CerCo cost annotating technology or, more generally, by the know- how provided in the certification of compilers. It is worth noting that several of these software houses are located in Europe, such as the medium-sized System Engineer Group of Freescale, which is headquartered in Scotland, Raisonance and Cosmic Software, which are headquartered in France, the small-size Hightech, headquartered in Germany, just to name a few.

\subsection{Management of knowledge and intellectual property}
All project partners have signed a Consortium Agreement before the start
of the project, setting the principles of the consortium management and
placing the relationship between the partners and their responsibilities on
a legal basis for the duration of the work. In particular, the agreement
includes specific arrangements concerning intellectual property rights to be
 applied among the participants and their affiliates, in compliance with the
general arrangements stipulated in the contract.
It thus specifies the rules
for dissemination and use (confidentiality, ownership of results, patent rights,
exploitation of results, protection and dissemination of knowledge), as well
as financial and legal provisions.
A peculiarity of \cerco{}
is that we self-constrained to release open source software only, which is
also manifest in our prototypes that will all be public, and that we did not
identify any background to be protected.

\subsection{Approach to Dissemination and Use}
The \cerco{} project represents an unprecedented effort to create a verified
chain of trust for intentional program properties during compilation,
and we thus expect that it will generate in the short term a large interest in
academia and in a longer term also a significant one in industry.

Dissemination and use of foreground will have a high priority that will be
intensified towards the end of the project and whose target will progressively
shift from academia to potential end users.
Work package 6 will be devoted to all the activities relevant to accomplishing this task.

    We have planned appropriate measures to ensure an effective and
timely dissemination of the project results to potential users, both at the European level and worldwide. Since the research started in \cerco{} is of the
long term kind, the main target of the dissemination activity will be research
institutions that can immediately benefit from our results and that should take
over the research effort after the end of \cerco{} to achieve the long terms
results. We will also target industry by means of specific dissemination actions
towards the end of the project in order to advertise our results and to ensure
that the final outcome fulfil actual requirements of the industrial community.

Dissemination will be carried out by a variety of means:
\begin{itemize}
 \item Talks at relevant international conferences, events and forums (both
       presenting the technical achievements and introducing at a high level
       the project’s objectives and results).
 \item Publication of papers in proceedings of international conferences and
       events, as well as in international scientific journals.
 \item Organization of meetings on project-related topics,
       including ``project workshops'' where attendance of external experts
       and professionals is based on invitation.
 \item Organization of at least one special event targeted to the scientific
       community, in the form of an open workshop, possibly affiliated to a
       major conference, or in the form of courses given at summer schools
       or equivalent teaching events targeted to Ph.D. students.
 \item Organization of at least one special even targeted to potential
       industrial stakeholders, in the form of a dissemination meeting to
       be hold during the last year of the project.
 \item Design and management of a publicly available web-site that includes
       descriptions of the main project results and allows the download of
       all the software and publications developed in \cerco. The web-site will
       be managed as a Wiki to maximise interaction with the community of
       users and researchers interested in the project.
 \item Press conferences and press releases describing the advancement and
       main results of the project, so to reach and make the public aware of
       both the short-term and long-term impact of the project results.
 \item Dissemination of project objectives and results to members of
       European or national level projects having \cerco{} members as
       participants.
\end{itemize}

\section{Description of the Dissemination Plan}
\subsection{Web presence and information exchange}
The website of the \cerco{} project is
\begin{center}\url{cerco.cs.unibo.it}\end{center}
and it is made of a combination of a private and a public Wiki.
The Wiki will progressively include:
\begin{itemize}
 \item A general introduction to the project: the objectives, the expected
      results, the milestones, the detailed description of the consortium and
      its coordinates within the Seventh Framework Programme.
 \item The list of events taking place in the context of the project: meetings,
      conferences, workshops, and their availability to the public.
 \item Publications originated from the project, both in the scientific community and in the general press.
 \item A number of relevant links: other projects, institutions and companies
      that are related to \cerco.
 \item A public section containing the public deliverables, comprising the
       open source software developed in \cerco. In order to make a first
       trial of the software as simple as possible for interested users,
       we plan to provide packages for some common Linux distributions and
       a Live CD for non Linux users.
 \item A private section containing the remaining deliverables and other
       documents for the European Commission.
 \item A private section containing contact details, mailing lists archives,
       details about the meetings (slides, notes and so on) and other
       temporary technical information needed by the consortium.
\end{itemize}

    Besides for the website, communication and information exchange among
the members of the project is enforced via a carefully organized and maintained central repository and a number of dynamically created mailing lists.

Ad-hoc advertisement of \cerco{} to the interested research communities will
also be achieved by advertisements sent to the mailing lists of the projects,
as well as advertisement of open job positions.

\subsection{Project Workshops and Conferences, Lectures, Tutorials}
Two Project Workshops will be organized every year.
They will consist in a public and a private chapter and we will invite as
guests a small number or international researchers who are working on related
problems. We will try to co-locate later workshops with international events
to improve visibility of the project. During the third year we plan as well to
organize two separate additional events targeted to the scientific community
and to potential industrial stakeholders.

Moreover, we aim to present our work at international conferences and
forums on interactive and automatic theorem proving, resource aware computing,
invariant generation, formal methods and reactive computing. In accordance
with the character of the corresponding meeting, the presentation of \cerco{}
may be part of a more comprehensive presentation, it may get a presentation of
its own, or even only special aspects of \cerco{} may be addressed by a talk.
In the latter case some member of the group caring about the relative task
or work-package may be the most suitable person to give the talk. Talks at
larger conferences should be accompanied by papers on \cerco{} in the corresponding proceedings.

\subsection{Publications}
We aim to publish the results obtained in \cerco{} in the proceedings
of international events and in international journals. The list of journals
that publish papers related to the topics studied in \cerco{} comprises and
it is not limited to the following ones:

\begin{itemize}
 \item Journal of Automated Reasoning
 \item Journal of Formalized Reasoning
 \item Information and Computation
 \item Higher-Order and Symbolic Computation
 \item Communications of the ACM
 \item Science of computer programming
\end{itemize}

Many international conferences and workshops deal with compilation,
formal reasonings and resource analysis. Some of the most important are
certainly

\begin{itemize}
 \item Principles of Programming Languages (POPL)
 \item Interactive Theorem Proving (ITP, ex TPHOLs)
 \item Logic for Programming, Artificial Intelligence and Reasoning (LPAR)
 \item Compiler Construction (CC)
 \item International Symposium on Formal Methods (FM)
 \item Symposium on Programming Languages and Reasoning (APLAS)
 %\item Types for Proofs and Programs (TYPEs)
\end{itemize}

\subsection{Clustering}

This section indicates some projects and organizations relevant to the ongoing work (at world-wide, European or national level) and with which information exchange might be beneficial.

\subsubsection{National/Local Projects and Research Groups}

The following national/local projects and research groups are the most direct
interlocutors for \cerco.

\begin{itemize}
 \item CompCert \url{http://compcert.inria.fr}, the most advanced, closed
       source project on the development of a certified compiler for a subset
       of C, and a natural source of inspiration and competitor for \cerco.
 \item Frama-C \url{http://frama-c.com}, an extensible and collaborative
       platform dedicated to source-code analysis of C software. It is a
       natural candidate for a technological integration with the \cerco{}
       compiler in order to provide high-level reasoning tools on the
       intentional properties of C programs.
 \item AbsInt \url{http://absint.com} is a privately-held company located
       in Saarbruecken, Germany, that participated to several EU projects and
       has a good record of collaboration with the scientific community. It
       develops advanced development tools for embedded systems, and tools for
       validation, verification and certification of safety-critical software.
\end{itemize}

\subsubsection{EU Projects}

This is a selection of EU projects (mainly from FP7) dealing with embedded or,
more generally, resource constrained systems.

\begin{itemize}
\item ARTEMIS: European Technology Platform/Joint Technology Initiative on
      Advanced Research \& Technology for Embedded Intelligence and Systems
\item Embounded: FP6 Strep on Automatic Analysis of Bounded Resources for Embedded Systems. 
\item ARTISTDesign: FP7 Network of Excellence on Design of Embedded Systems
\item MNEMEE : FP7 Collaborative Project on Memory management technology for adaptive and efficient design of embedded systems. Jan 2008 -- Dec 2010.
\item INTERESTED: FP7 Collaborative Project on Interoperable embedded systems Tool-chain for enhanced rapid design, prototyping and code generation. Jan 2008 -- Dec 2010.
\item PREDATOR : FP7 Collaborative Project on Design for predictability and efficiency. Feb 2008 -- Jan 2011.
\item QUASIMODO : FP7 Collaborative Project on Quantitative system properties in model-driven design of embedded systems. Jan 2008 -- Dec 2010.
\end{itemize}

\section{Description of the Use Plan (by result)}\label{byresult}

In this section, we describe the expected project results that are released
in correspondence with project milestones and that have potential
for exploitation.

\subsection{Untrusted cost-annotating compiler}
\textbf{Delivery date:} January 2011\\
\textbf{Description:}
The untrusted cost-annotating compiler will be a functional compiler from
a large subset of C to some assembly language. It will already trace the
evolution of selected high-level code fragments in order to relate them to
low level code fragments and it will manifest cost annotations in the source
language.\\
\textbf{Target communities:} compiler developers; developers of code invariant
generators; developers of tools for cache behaviour prediction and general
analysis of assembly code.\\

Compiler developers will be interested by the techniques used to trace evolution
of code fragments during compilation. They should also be interested in
enhancing the proposed techniques to address more optimizations.

Developers of code invariant generators will be able to apply and extend their
own techniques to deal with exact execution time by considering cost annotations
during the invariant generation phase. 

Developers of tools for cache behaviour prediction and general analysis of
assembly code should be particularly interested since our approach allows to
reflect on the source code their own analysis performed on low level target
code.

\noindent
\textbf{Dissemination:} Information dissemination on this activity will be done
on the general project level, but will also try to target specific communities
by targeted presentations/participation to relative conferences or meetings.
In particular we plan to invite selected members of those communities to the
first annual \cerco{} meeting to advertise the project results and foster
potential collaborations.

\subsection{Untrusted CerCo compiler}
\textbf{Delivery date:} January 2012\\
\textbf{Description:}
The CerCo compiler will be a re-implementation of the untrusted cost-annotating
compiler in the variant of the Calculus of (Co)Inductive Constructions
implemented by Matita, ready to be certified. Moreover, it will enhance the
previous prototype by integrating a new layer for the management of cost
annotations (produced by the compiler) and the complexity assertions (added
by the user or synthesized automatically by abstract interpretation algorithms)
in order to produce the right complexity obligations, that is the goal to be
proved in order to check the correctness of the assertions.\\
\textbf{Target communities:} the interactive theorem proving community;
developers of code invariant generators; the abstract interpretation
community; end users.\\

The interactive theorem proving community will benefit from an executable
specification of a realistic compiler for C written in
the Calculus of (Co)Inductive Constructions. However, at this stage the
main benefit for the community will be a project by-product, which is
a low level executable semantics (an interpreter) for some
target machine and for several intermediate languages, that could easily be
reused in other formalizations and translated to other interactive theorem
provers.

Developers of code invariant generators and the abstract interpretation
community should be interested in the new layer of management of cost
annotations and complexity assertions in order to interface their techniques on
top of it or to propose alternative management approaches. The prototype could
also be used as a test-bench generator for their techniques.

Starting with the release of the prototype we will begin to contact potential
end users, i.e. developers of time critical software, in order to attract
feedback and to ensure that the final outcome fulfil actual requirements of
the targeted exploitation community.

\noindent
\textbf{Dissemination:} Information dissemination on this activity will be done
on the general project level, with particular attention to the interactive
theorem proving community. We will continue the practice of inviting
selected members of the interested communities to the
annual \cerco{} meetings to advertise the project results and foster
potential collaborations. Moreover we will gradually enlarge the scope of the
dissemination activity from developers and researchers in formal methods to
the wider audience of users of compilers that are potentially interested in
exact execution time, even if at this stage we do not expect
applications of the prototype to realistic programs.

\subsection{Trusted CerCo compiler}
\textbf{Delivery date:} January 2013\\
\textbf{Description:}
The trusted CerCo compiler is the final prototype of \cerco{} and it is
composed of several components
\begin{itemize}
 \item a proof of correctness in Matita of the
compliance of the compiler, described as preservation of both the extensional
and intensional behaviour of the program;
 \item an extension of the interactive
theorem prover Matita with ad-hoc tactics and mechanism targeted towards the
progressive automation --- either in the small or in the large --- of complexity
proofs;
 \item an extensive use case dedicated to the automatic generation of
cost invariants for the C code generated by a synchronous language compiler.
The functionalities developed in the use case will be tested to compute
certified reaction time bounds for significant examples of synchronous
programs.
\end{itemize}
\textbf{Target communities:} the interactive and automatic theorem proving
community; developers of code invariant generators; end users, in particular
synchronous languages programmers.\\

The interactive theorem proving community will benefit from the first fully
open source proof of correctness of a realistic compiler for C written in
the Calculus of (Co)Inductive Constructions and for a new technique to formally
verify preservation of intentional properties without loosing precision.
Developers of both interactive and automatic theorem provers will be interested
in testing and enhancing their techniques when applied to automation of
complexity proofs.

The final prototype of the \cerco{} project is supposed to be the first
realistic milestone towards the formal certification of exact execution time 
(or exact reaction time) for real time or synchronous programs and thus
it is meant to attract interest from end users. In particular, we will be
looking for feedback on the applicability of the proposed technique and we
will target in particular the sub-community of synchronous programmers.

\noindent
\textbf{Dissemination:} We will increase our dissemination activity during the
last year of the project, in particular organizing separate events targeted to
the scientific community and to the potential industrial stakeholders. We will
also improve accessibility and visibility of the \cerco{} compiler by developing
packages for Linux distributions and Live CDs for non-Linux users.

%\begin{thebibliography}{9}
%\bibitem{matita} The Interactive Theorem Prover Matita,
% \url{http://matita.cs.unibo.it}
%\bibitem{subversion}The Version Control System Subversion,
% \url{http://subversion.apache.org}
%\bibitem{trac}The Integrated SCM \& Project Management tool Trac,
% \url{http://trac.edgewall.org}
%\end{thebibliography}

\end{document}