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

Last change on this file since 47 was 47, checked in by mulligan, 11 years ago

Half of report's English fixed.

File size: 28.1 KB
8\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
10\date{ }
30Report n. D6.2\\
31Plan for the Use and dissemination of foreground\\
38Version 1.0
45Main Authors:\\
46C. Sacerdoti Coen
52Project Acronym: \cerco{}\\
53Project full title: Certified Complexity\\
54Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
56\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
61The deliverable D6.2 \emph{Plan for the Use and dissemination of foreground}
62is the first \textbf{report} of the \cerco{} project. The deliverable is
63\textbf{confidential} and required an effort of about \textbf{2 person-months}.
64The following is a description of the deliverable in the Grant Agreement:
66Plan for the Use and dissemination of foreground: An articulated dissemination plan, containing the individuation of the main target communities, and the relative exploitation strategies.
71%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.
73%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.
75%3. Exploitable results
77%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.
79%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:
81%    * 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);
83%    * Customer detection: identification of the potential customers and the factors that affect their purchasing decisions;
85%    * 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;
87%    * 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.
89%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.
92\section{Overview and General Approach}
93\subsection{Overview of expected results}
94Driven by a growing confidence in formal methods in general and interactive
95theorem proving in particular, critical IT systems are slowly undergoing a
96paradigm shift: testing of critical properties is going to be partially
97replaced with formal verification of programs written in high level
98languages, and a set of formally verified tools (interpreters, compilers,
99operating systems, communication libraries) is going to be used to preserve
100the verified properties for the execution of the low level code.
102The present state of the art already provides a few mildly optimizing
103verified compilers that compete with traditional highly optimised compilers,
104and a few prototypes and experiments in the verification of operating systems.
105However, the only properties that have been formalized are extensional, proving
106that the high level semantics of the program---usually specified in terms
107of infinite resources (e.g. memory)---is respected. All intensional
108properties that refer to resource consumption are not currently preserved during
109compilation or, at least, no formal proof of preservation is provided. Hence
110high level programs still need to be extensively tested to verify resource
111related properties like memory consumption or reaction time for reactive
112and real time programs.
114In \cerco{} we will address intentional properties of programs, in particular
115execution time, and we will develop the first certified compiler that is able
116to manifest in the source program some intentional properties, mainly
117execution cost, that are inferred from the target program. The main challenge is
118to preserve the compositionality of compilation: whilst the source program
119undergoes several intentionally disruptive translations toward lower and lower
120level intermediate languages, we must keep track of the evolution of
121sensible code fragments in order to relate source, intermediate and target
122code fragments, so that execution costs may be back-propagated. Hence we expect
123to study new more refined ways of expressing the operational semantics of
124programs and to give a more refined notion of operational bisimulation, with the
125aim of obtaining a characterisation that is loose enough to capture some of the
126most common and effective optimisations.
128Once we can manifest in the source program execution costs computed on the
129target program we will start investigating the exploitability of the
130cost annotations. In particular, cost annotations must be combined with
131extensional program invariants in order to obtain intensional program invariants,
132and be able to formally prove intensional properties of programs. We expect
133this study to require a long effort and to be performed outside the project
134timeframe. However, we assume that a combination of interactive theorem proving
135and automatated formal methods (like abstract interpretation) will need to be
136exploited and, in the project, we will focus on interactive theorem proving by
137exploiting and providing basic tools to reason about cost invariants.
139All the major deliverables of \cerco{} are prototypes---either software
140prototypes or formal certifications---that are later integrated at project
141milestones into major \cerco{} compiler snapshots. These snapshots are the
142most appropriate deliverables for dissemination in the large, and different
143target communities are associated to the snapshots. We will discuss
144the milestones and snapshots in detail in Section~\ref{byresult} in order to
145identify the potential target communities and most appropriate means of
154Milestone name & Month due \\ \hline
155Untrusted cost-annotating compiler & 12 \\
156Untrusted CerCo compiler & 24 \\
157Trusted CerCo compiler & 36 \\
164\subsection{Academic exploitation}
165 Academic partners will take great advantage of the \cerco{}'s results mainly in
166terms of increased technical know-how and scientific knowledge, increased
167visibility in the scientific community of reference, increased expertise,
168and for institutional academic exploitation (e.g. didactic activities). We also
169expect that the rest of the academic community will take up the innovative ideas
170of the project, building on top of them code analyses at a level of accuracy that
171could have not been previously possible. Finally, we expect our methodology to
172be applied to other styles of high-level programming language (for instance,
173functional or logic) and to more complex scenarios involving, for example, a
174real time operating system.
176\subsection{Industrial exploitation}
177The long term industrial exploitation of the results of the CerCo project is
178mainly embodied in the area of embedded systems/software, in particular in the
179case of safety critical applications and time critical (realtime) applications.
180In the short term, software houses producing compilers for embedded systems
181could immediately draw benefit from the \cerco{} cost annotating technology or,
182more generally, by the knowledge gained in the certification of compilers. It
183is worth noting that several of these software houses are located in Europe,
184such as the medium-scale System Engineer Group of Freescale, headquartered in
185Scotland, Raisonance and Cosmic Software, headquartered in France, and the
186small-scale Hightech, headquartered in Germany, amongst many others.
188\subsection{Management of knowledge and intellectual property}
189All project partners have signed a Consortium Agreement before the start
190of the project, setting the principles of the consortium management and
191placing the relationship between the partners and their responsibilities on
192a legal basis for the duration of the work. In particular, the agreement
193includes specific arrangements concerning intellectual property rights to be
194 applied among the participants and their affiliates, in compliance with the
195general arrangements stipulated in the contract.
196It thus specifies the rules
197for dissemination and use (confidentiality, ownership of results, patent rights,
198exploitation of results, protection and dissemination of knowledge), as well
199as financial and legal provisions.
200A peculiarity of \cerco{}
201is that we self-constrained to release open source software only, which is
202also manifest in our prototypes that will all be public, and that we did not
203identify any background to be protected.
205\subsection{Approach to Dissemination and Use}
206The \cerco{} project represents an unprecedented effort to create a verified
207chain of trust for intentional program properties during compilation,
208and we thus expect that it will generate in the short term a large interest in
209academia and in a longer term also a significant one in industry.
211Dissemination and use of foreground will have a high priority that will be
212intensified towards the end of the project and whose target will progressively
213shift from academia to potential end users.
214Work package 6 will be devoted to all the activities relevant to accomplishing this task.
216    We have planned appropriate measures to ensure an effective and
217timely dissemination of the project results to potential users, both at the European level and worldwide. Since the research started in \cerco{} is of the
218long term kind, the main target of the dissemination activity will be research
219institutions that can immediately benefit from our results and that should take
220over the research effort after the end of \cerco{} to achieve the long terms
221results. We will also target industry by means of specific dissemination actions
222towards the end of the project in order to advertise our results and to ensure
223that the final outcome fulfil actual requirements of the industrial community.
225Dissemination will be carried out by a variety of means:
227 \item Talks at relevant international conferences, events and forums (both
228       presenting the technical achievements and introducing at a high level
229       the project’s objectives and results).
230 \item Publication of papers in proceedings of international conferences and
231       events, as well as in international scientific journals.
232 \item Organization of meetings on project-related topics,
233       including ``project workshops'' where attendance of external experts
234       and professionals is based on invitation.
235 \item Organization of at least one special event targeted to the scientific
236       community, in the form of an open workshop, possibly affiliated to a
237       major conference, or in the form of courses given at summer schools
238       or equivalent teaching events targeted to Ph.D. students.
239 \item Organization of at least one special even targeted to potential
240       industrial stakeholders, in the form of a dissemination meeting to
241       be hold during the last year of the project.
242 \item Design and management of a publicly available web-site that includes
243       descriptions of the main project results and allows the download of
244       all the software and publications developed in \cerco. The web-site will
245       be managed as a Wiki to maximise interaction with the community of
246       users and researchers interested in the project.
247 \item Press conferences and press releases describing the advancement and
248       main results of the project, so to reach and make the public aware of
249       both the short-term and long-term impact of the project results.
250 \item Dissemination of project objectives and results to members of
251       European or national level projects having \cerco{} members as
252       participants.
255\section{Description of the Dissemination Plan}
256\subsection{Web presence and information exchange}
257The website of the \cerco{} project is
259and it is made of a combination of a private and a public Wiki.
260The Wiki will progressively include:
262 \item A general introduction to the project: the objectives, the expected
263      results, the milestones, the detailed description of the consortium and
264      its coordinates within the Seventh Framework Programme.
265 \item The list of events taking place in the context of the project: meetings,
266      conferences, workshops, and their availability to the public.
267 \item Publications originated from the project, both in the scientific community and in the general press.
268 \item A number of relevant links: other projects, institutions and companies
269      that are related to \cerco.
270 \item A public section containing the public deliverables, comprising the
271       open source software developed in \cerco. In order to make a first
272       trial of the software as simple as possible for interested users,
273       we plan to provide packages for some common Linux distributions and
274       a Live CD for non Linux users.
275 \item A private section containing the remaining deliverables and other
276       documents for the European Commission.
277 \item A private section containing contact details, mailing lists archives,
278       details about the meetings (slides, notes and so on) and other
279       temporary technical information needed by the consortium.
282    Besides for the website, communication and information exchange among
283the members of the project is enforced via a carefully organized and maintained central repository and a number of dynamically created mailing lists.
285Ad-hoc advertisement of \cerco{} to the interested research communities will
286also be achieved by advertisements sent to the mailing lists of the projects,
287as well as advertisement of open job positions.
289\subsection{Project Workshops and Conferences, Lectures, Tutorials}
290Two Project Workshops will be organized every year.
291They will consist in a public and a private chapter and we will invite as
292guests a small number or international researchers who are working on related
293problems. We will try to co-locate later workshops with international events
294to improve visibility of the project. During the third year we plan as well to
295organize two separate additional events targeted to the scientific community
296and to potential industrial stakeholders.
298Moreover, we aim to present our work at international conferences and
299forums on interactive and automatic theorem proving, resource aware computing,
300invariant generation, formal methods and reactive computing. In accordance
301with the character of the corresponding meeting, the presentation of \cerco{}
302may be part of a more comprehensive presentation, it may get a presentation of
303its own, or even only special aspects of \cerco{} may be addressed by a talk.
304In the latter case some member of the group caring about the relative task
305or work-package may be the most suitable person to give the talk. Talks at
306larger conferences should be accompanied by papers on \cerco{} in the corresponding proceedings.
309We aim to publish the results obtained in \cerco{} in the proceedings
310of international events and in international journals. The list of journals
311that publish papers related to the topics studied in \cerco{} comprises and
312it is not limited to the following ones:
315 \item Journal of Automated Reasoning
316 \item Journal of Formalized Reasoning
317 \item Information and Computation
318 \item Higher-Order and Symbolic Computation
319 \item Communications of the ACM
320 \item Science of computer programming
323Many international conferences and workshops deal with compilation,
324formal reasonings and resource analysis. Some of the most important are
328 \item Principles of Programming Languages (POPL)
329 \item Interactive Theorem Proving (ITP, ex TPHOLs)
330 \item Logic for Programming, Artificial Intelligence and Reasoning (LPAR)
331 \item Compiler Construction (CC)
332 \item International Symposium on Formal Methods (FM)
333 \item Symposium on Programming Languages and Reasoning (APLAS)
334 %\item Types for Proofs and Programs (TYPEs)
339This 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.
341\subsubsection{National/Local Projects and Research Groups}
343The following national/local projects and research groups are the most direct
344interlocutors for \cerco.
347 \item CompCert \url{}, the most advanced, closed
348       source project on the development of a certified compiler for a subset
349       of C, and a natural source of inspiration and competitor for \cerco.
350 \item Frama-C \url{}, an extensible and collaborative
351       platform dedicated to source-code analysis of C software. It is a
352       natural candidate for a technological integration with the \cerco{}
353       compiler in order to provide high-level reasoning tools on the
354       intentional properties of C programs.
355 \item AbsInt \url{} is a privately-held company located
356       in Saarbruecken, Germany, that participated to several EU projects and
357       has a good record of collaboration with the scientific community. It
358       develops advanced development tools for embedded systems, and tools for
359       validation, verification and certification of safety-critical software.
362\subsubsection{EU Projects}
364This is a selection of EU projects (mainly from FP7) dealing with embedded or,
365more generally, resource constrained systems.
368\item ARTEMIS: European Technology Platform/Joint Technology Initiative on
369      Advanced Research \& Technology for Embedded Intelligence and Systems
370\item Embounded: FP6 Strep on Automatic Analysis of Bounded Resources for Embedded Systems.
371\item ARTISTDesign: FP7 Network of Excellence on Design of Embedded Systems
372\item MNEMEE : FP7 Collaborative Project on Memory management technology for adaptive and efficient design of embedded systems. Jan 2008 -- Dec 2010.
373\item INTERESTED: FP7 Collaborative Project on Interoperable embedded systems Tool-chain for enhanced rapid design, prototyping and code generation. Jan 2008 -- Dec 2010.
374\item PREDATOR : FP7 Collaborative Project on Design for predictability and efficiency. Feb 2008 -- Jan 2011.
375\item QUASIMODO : FP7 Collaborative Project on Quantitative system properties in model-driven design of embedded systems. Jan 2008 -- Dec 2010.
378\section{Description of the Use Plan (by result)}\label{byresult}
380In this section, we describe the expected project results that are released
381in correspondence with project milestones and that have potential
382for exploitation.
384\subsection{Untrusted cost-annotating compiler}
385\textbf{Delivery date:} January 2011\\
387The untrusted cost-annotating compiler will be a functional compiler from
388a large subset of C to some assembly language. It will already trace the
389evolution of selected high-level code fragments in order to relate them to
390low level code fragments and it will manifest cost annotations in the source
392\textbf{Target communities:} compiler developers; developers of code invariant
393generators; developers of tools for cache behaviour prediction and general
394analysis of assembly code.\\
396Compiler developers will be interested by the techniques used to trace evolution
397of code fragments during compilation. They should also be interested in
398enhancing the proposed techniques to address more optimisations.
400Developers of code invariant generators will be able to apply and extend their
401own techniques to deal with exact execution time by considering cost annotations
402during the invariant generation phase.
404Developers of tools for cache behaviour prediction and general analysis of
405assembly code should be particularly interested since our approach allows to
406reflect on the source code their own analysis performed on low level target
410\textbf{Dissemination:} Information dissemination on this activity will be done
411on the general project level, but will also try to target specific communities
412by targeted presentations/participation to relative conferences or meetings.
413In particular we plan to invite selected members of those communities to the
414first annual \cerco{} meeting to advertise the project results and foster
415potential collaborations.
417\subsection{Untrusted CerCo compiler}
418\textbf{Delivery date:} January 2012\\
420The CerCo compiler will be a re-implementation of the untrusted cost-annotating
421compiler in the variant of the Calculus of (Co)Inductive Constructions
422implemented by Matita, ready to be certified. Moreover, it will enhance the
423previous prototype by integrating a new layer for the management of cost
424annotations (produced by the compiler) and the complexity assertions (added
425by the user or synthesized automatically by abstract interpretation algorithms)
426in order to produce the right complexity obligations, that is the goal to be
427proved in order to check the correctness of the assertions.\\
428\textbf{Target communities:} the interactive theorem proving community;
429developers of code invariant generators; the abstract interpretation
430community; end users.\\
432The interactive theorem proving community will benefit from an executable
433specification of a realistic compiler for C written in
434the Calculus of (Co)Inductive Constructions. However, at this stage the
435main benefit for the community will be a project by-product, which is
436a low level executable semantics (an interpreter) for some
437target machine and for several intermediate languages, that could easily be
438reused in other formalizations and translated to other interactive theorem
441Developers of code invariant generators and the abstract interpretation
442community should be interested in the new layer of management of cost
443annotations and complexity assertions in order to interface their techniques on
444top of it or to propose alternative management approaches. The prototype could
445also be used as a test-bench generator for their techniques.
447Starting with the release of the prototype we will begin to contact potential
448end users, i.e. developers of time critical software, in order to attract
449feedback and to ensure that the final outcome fulfil actual requirements of
450the targeted exploitation community.
453\textbf{Dissemination:} Information dissemination on this activity will be done
454on the general project level, with particular attention to the interactive
455theorem proving community. We will continue the practice of inviting
456selected members of the interested communities to the
457annual \cerco{} meetings to advertise the project results and foster
458potential collaborations. Moreover we will gradually enlarge the scope of the
459dissemination activity from developers and researchers in formal methods to
460the wider audience of users of compilers that are potentially interested in
461exact execution time, even if at this stage we do not expect
462applications of the prototype to realistic programs.
464\subsection{Trusted CerCo compiler}
465\textbf{Delivery date:} January 2013\\
467The trusted CerCo compiler is the final prototype of \cerco{} and it is
468composed of several components
470 \item a proof of correctness in Matita of the
471compliance of the compiler, described as preservation of both the extensional
472and intensional behaviour of the program;
473 \item an extension of the interactive
474theorem prover Matita with ad-hoc tactics and mechanism targeted towards the
475progressive automation --- either in the small or in the large --- of complexity
477 \item an extensive use case dedicated to the automatic generation of
478cost invariants for the C code generated by a synchronous language compiler.
479The functionalities developed in the use case will be tested to compute
480certified reaction time bounds for significant examples of synchronous
483\textbf{Target communities:} the interactive and automatic theorem proving
484community; developers of code invariant generators; end users, in particular
485synchronous languages programmers.\\
487The interactive theorem proving community will benefit from the first fully
488open source proof of correctness of a realistic compiler for C written in
489the Calculus of (Co)Inductive Constructions and for a new technique to formally
490verify preservation of intentional properties without loosing precision.
491Developers of both interactive and automatic theorem provers will be interested
492in testing and enhancing their techniques when applied to automation of
493complexity proofs.
495The final prototype of the \cerco{} project is supposed to be the first
496realistic milestone towards the formal certification of exact execution time
497(or exact reaction time) for real time or synchronous programs and thus
498it is meant to attract interest from end users. In particular, we will be
499looking for feedback on the applicability of the proposed technique and we
500will target in particular the sub-community of synchronous programmers.
503\textbf{Dissemination:} We will increase our dissemination activity during the
504last year of the project, in particular organizing separate events targeted to
505the scientific community and to the potential industrial stakeholders. We will
506also improve accessibility and visibility of the \cerco{} compiler by developing
507packages for Linux distributions and Live CDs for non-Linux users.
510%\bibitem{matita} The Interactive Theorem Prover Matita,
511% \url{}
512%\bibitem{subversion}The Version Control System Subversion,
513% \url{}
514%\bibitem{trac}The Integrated SCM \& Project Management tool Trac,
515% \url{}
Note: See TracBrowser for help on using the repository browser.