Last change on this file since 1948 was 794, checked in by Ian Stark, 10 years ago

• Property svn:eol-style set to native
• Property svn:executable set to *
• Property svn:mime-type set to text/x-latex
File size: 8.0 KB
Line
1% CerCo: Certified Complexity
2%
4%
5% Plan for Dissemination and Use
6% Addendum requested by project reviewers at end of year 1.
7%
8% Ian Stark
9% 2011-05
10
11\documentclass[11pt,a4paper]{article}
12\usepackage{../style/cerco}
13
14\hypersetup{bookmarksopenlevel=2}
15
16\title{
17INFORMATION AND COMMUNICATION TECHNOLOGIES\\
18(ICT)\\
19PROGRAMME\\
20\vspace*{1cm}Project FP7-ICT-2009-C-243881 {\cerco}}
21
22\date{ }
23\author{}
24
25\begin{document}
26\thispagestyle{empty}
27
28\vspace*{-1cm}
29\begin{center}
30\includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
31\end{center}
32
33\begin{minipage}{\textwidth}
34\maketitle
35\end{minipage}
36
37
38\vspace*{0.5cm}
39\begin{center}
40\begin{LARGE}
41\bf
43Future Dissemination Plans
44\end{LARGE}
45\end{center}
46
47\vspace*{2cm}
48\begin{center}
49\begin{large}
50Version 1.0
51\end{large}
52\end{center}
53
54\vspace*{0.5cm}
55\begin{center}
56\begin{large}
57Main Authors:\\
58I. Stark
59\end{large}
60\end{center}
61
62\vspace*{\fill}
63\noindent
64Project Acronym: {\cerco}\\
65Project full title: Certified Complexity\\
66Proposal/Contract no.: FP7-ICT-2009-C-243881 {\cerco}\\
67
69
70\tableofcontents
71
72\section{Premise}
73Deliverable~6.2, the \emph{Plan for the Use and Dissemination of Foreground}
74was submitted as the first report of the {\cerco} project.  Following the
75scientific review of the project at the end of its first year, the reviewers
76recommended preparation of an addendum to specifically list future
77dissemination plans.  This is that addendum.
78
79
80\section{Dissemination Plans}
81
82The {\cerco} project represents an unprecedented effort to create a
83machine-verified chain of trust for analysing program performance properties
84through compilation.  This combines novel work in the theory of machine proof
85and certified compilation with its concrete application to a specific
86industrial microcontroller.
87
88As appropriate for a project in the \emph{Future and Emerging Technologies}
89programme, a major target for dissemination is to influence future work by
90other European research groups, through a direct demonstration of a verified
91resource-aware compiler.  The immediate routes for this are the standard ones
92for academic communication and training: conference papers, journal articles,
93collaborative workshops, tutorial events.  In addition, with the project
94centred around a substantial implementation effort, the compiler code and the
95machine proofs are themselves vehicles for dissemination to other researchers.
96
97The longer-term dissemination targets are the potential end-users of verified
98compiler technology: programmers of commodity microcontrollers being used in
99tightly resource-constrained embedded applications --- particularly those
100where safety-critical requirements mandate a high quality of performance
101certification.  Possible routes for this long-term dissemination are through
102research symposia at industrially-relevant conferences, and tutorial sessions
103at conferences or other events with significant industrial presence.
104
105\subsection{Conferences and Workshops}
106
107We propose to submit results of {\cerco} research for presentation at
108appropriate international venues.  There are very many conferences dealing
109with {\cerco}-related areas: compilation technology, machine-assisted proof,
110resource analysis, etc.  For example, the following are particularly close to
111{\cerco} activity:
112\begin{itemize}
113\item CPP: Certified Programs and Proofs
114\item FMCAD: Formal Methods in Computer-Aided Design
115\item LOLA: Syntax and Semantics of Low-Level Languages
116\item VSTTE: Verified Software: Theories, Tools and Experiments
117\item SSV: Systems Software Verification
118\item FORMATS: Formal Modeling and Analysis of Timed Systems
119\item ITP: Interactive Theorem Proving (was TPHOLs)
120\item PSI: Program Understanding
121\end{itemize}
122Beyond these, there are many high-quality general conferences which would also
123provide a good venue for publicising the results of the project.  For example:
124\begin{itemize}
125\item POPL: Principles of Programming Languages
126\item LPAR: Logic for Programming, Artificial Intelligence and Reasoning
127\item CC: Compiler Construction
128\item FM: International Symposium on Formal Methods
129\item APLAS: Asian Symposium on Programming Languages and Reasoning
130\end{itemize}
131In addition to these subject-related events, {\cerco} will contribute to
132FET-organized activities, such as conferences, dedicated workshops, working
133groups and other meetings.
134
135
136\subsection{Journals}
137
138The project participants will publish papers and articles based on {\cerco}
139results in appropriate archival venues, throughout the duration of the
140project.  Most of the conferences listed above have formal proceedings;
141several also have affiliated special issues in journals, for publishing
142extended versions of papers.  In addition, we expect to submit free-standing
143articles to appropriate journals, such as:
144\begin{itemize}
145\item Journal of Automated Reasoning
146\item Journal of Formalized Reasoning
147\item Information and Computation
148\item Theoretical Computer Science
149\item Higher-Order and Symbolic Computation
150\item Communications of the ACM
151\item Science of Computer Programming
152\end{itemize}
153
154\subsection{Tutorials and Training}
155
156As established researchers, the project participants will give lectures and
157tutorials on {\cerco}-related research as part of their existing dissemination
158activity throughout the course of the project.  However, in addition to this
159{\cerco} will organise specific training activities targeted at the scientific
160community, and at potential industrial stakeholders.  These are formal
161deliverables of Work Package~6 in the project contract.  To increase
162visibility, and promote attendance, we would affiliate any event with an
163existing conference or school.  For example, a {\cerco} tutorial would much
164more effectively reach a suitable audience if given as part of an established
165summer school.  It may also be appropriate to collaborate with related EU
166projects or research groups in management of such events.
167
168To benefit the most from {\cerco} project results, such events should take
169place in the final year of the project.  We plan to identify appropriate
170venues during the second year of {\cerco}.
171
172\subsection{Artefacts}
173
174A significant part of {\cerco} is the implementation effort, with accompanying
175experience gained in developing and verifying a machine-checked resource-aware
176compiler.  This gives rise to specific software artefacts, which other
177projects can learn from and build upon.  All these will be made
178publically-available at project milestones, and form a notable route for
179dissemination of the project outcomes.  The full report D6.2 describes in
180detail the target communities and potential users of this software; here we
181summarize.
182
183\subsubsection{Untrusted Cost-Annotating Compiler}
184
185This is a functional compiler from C to assembler, structured and instrumented
186to trace the evolution of high-level code fragments to low-level instruction
187sequences and match their execution costs.
188
189\subsubsection{Untrusted Compiler within Proof-Assistant}
190
191This will be an implementation of the CerCo cost-annotating compiler within
192the \emph{Matita} proof assistant.  This takes the form of a formal
193specification of the compiler in the calculus of (co)inductive constructions,
194arranged in so as to be directly executable within \emph{Matita}
195
196\subsubsection{Trusted Cost-Annotating Compiler}
197
198This is the final product of the {\cerco} project and brings together a number
199of distinct elements:
200\begin{itemize}
201\item An executable compiler which automatically annotates C source code with
202  machine execution costs;
203\item A machine-certified proof that the compiler is functionally correct and
204  that the automatic annotations exactly reflect low-level instruction costs;
205\item Extensions to the \emph{Matita} interactive proof engine to automate
206  this substantial proof;
207\item Example integration of these low-level cost-annotations with high-level
208  program analysis tools in the \emph{Frama-C} framework.
209\end{itemize}
210
211
212\end{document}
213
214% LocalWords:  Sacerdoti Coen microcontroller FMCAD VSTTE TPHOLs LPAR Artefacts
Note: See TracBrowser for help on using the repository browser.