Changeset 794 for Deliverables/D6.2

Timestamp:

May 12, 2011, 7:19:02 PM (9 years ago)

Author:

Ian Stark

Message:

Some content for addendum

File:

• Deliverables/D6.2/addendum.tex (modified) (5 diffs)

Deliverables/D6.2/addendum.tex

@@ -9 +9 @@
 % 2011-05
 
-\documentclass[11pt,epsf,a4wide]{article}
+\documentclass[11pt,a4paper]{article}
 \usepackage{../style/cerco}
+
+\hypersetup{bookmarksopenlevel=2}
 
 \title{
@@ -16 +18 @@
 (ICT)\\
 PROGRAMME\\
-\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
+\vspace*{1cm}Project FP7-ICT-2009-C-243881 {\cerco}}
 
 \date{ }
@@ -54 +56 @@
 \begin{large}
 Main Authors:\\
-C. Sacerdoti Coen\\
 I. Stark
 \end{large}
@@ -61 +62 @@
 \vspace*{\fill}
 \noindent
-Project Acronym: \cerco{}\\
+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}
+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 \textbf{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
+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.
 
@@ -79 +80 @@
 \section{Dissemination Plans}
 
-\subsection{Conferences}
-
+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}
 
-\subsection{Workshops}
-
-\subsection{Tutorials}
+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