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

Last change on this file since 22 was 22, checked in by sacerdot, 11 years ago

Proposed final version.

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 description of the deliverable in the Grant Agreement is the following one:
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 on the programs written in an high level
98language, and a set of formally verified tools (interpreters, compilers,
99operating systems, communication libraries) is going to be used to grant preservation
100of the verified property for the actual runs of the low level code.
102The present state of the art already provides a few mildly optimizing
103verified compilers that compete with traditional highly optimized compilers
104and a few prototypes and experiments in the verification of operating systems.
105However, the only properties that have been formalized are extensional, granting
106that the high level semantics of the program --- usually specified in terms
107of infinite resources (e.g. memory) --- is respected. All intensional
108properties that have to do with resources 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 issue
118in doing so is to preserve compositionality of compilation: while the source
119program undergoes several intentionally disruptive translations towards lower
120and lower intermediate languages, we need to keep trace of the evolution of
121sensible code fragments in order to relate source, intermediate and target
122code fragments to back-propagate execution costs. Hence we expect to study
123new more refined ways of expressing the operational semantics of programs
124and to give a more refined notion of operational bisimulation, with the aim
125of obtaining a characterization that is loose enough to capture some of the
126most common and effective optimizations.
128Once we can manifest in the source program execution costs computed on the
129target program we will start the investigation of 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 automatic 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 on 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 details
145in Section~\ref{byresult} in order to identify the potential target communities
146and relative specific dissemination actions.
154milestone name & due at month \\ \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 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.
167\subsection{Industrial exploitation}
168 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.
170\subsection{Management of knowledge and intellectual property}
171All project partners have signed a Consortium Agreement before the start
172of the project, setting the principles of the consortium management and
173placing the relationship between the partners and their responsibilities on
174a legal basis for the duration of the work. In particular, the agreement
175includes specific arrangements concerning intellectual property rights to be
176 applied among the participants and their affiliates, in compliance with the
177general arrangements stipulated in the contract.
178It thus specifies the rules
179for dissemination and use (confidentiality, ownership of results, patent rights,
180exploitation of results, protection and dissemination of knowledge), as well
181as financial and legal provisions.
182A peculiarity of \cerco{}
183is that we self-constrained to release open source software only, which is
184also manifest in our prototypes that will all be public, and that we did not
185identify any background to be protected.
187\subsection{Approach to Dissemination and Use}
188The \cerco{} project represents an unprecedented effort to create a verified
189chain of trust for intentional program properties during compilation,
190and we thus expect that it will generate in the short term a large interest in
191academia and in a longer term also a significant one in industry.
193Dissemination and use of foreground will have a high priority that will be
194intensified towards the end of the project and whose target will progressively
195shift from academia to potential end users.
196Work package 6 will be devoted to all the activities relevant to accomplishing this task.
198    We have planned appropriate measures to ensure an effective and
199timely dissemination of the project results to potential users, both at the European level and worldwide. Since the research started in \cerco{} is of the
200long term kind, the main target of the dissemination activity will be research
201institutions that can immediately benefit from our results and that should take
202over the research effort after the end of \cerco{} to achieve the long terms
203results. We will also target industry by means of specific dissemination actions
204towards the end of the project in order to advertise our results and to ensure
205that the final outcome fulfil actual requirements of the industrial community.
207Dissemination will be carried out by a variety of means:
209 \item Talks at relevant international conferences, events and forums (both
210       presenting the technical achievements and introducing at a high level
211       the project’s objectives and results).
212 \item Publication of papers in proceedings of international conferences and
213       events, as well as in international scientific journals.
214 \item Organization of meetings on project-related topics,
215       including ``project workshops'' where attendance of external experts
216       and professionals is based on invitation.
217 \item Organization of at least one special event targeted to the scientific
218       community, in the form of an open workshop, possibly affiliated to a
219       major conference, or in the form of courses given at summer schools
220       or equivalent teaching events targeted to Ph.D. students.
221 \item Organization of at least one special even targeted to potential
222       industrial stakeholders, in the form of a dissemination meeting to
223       be hold during the last year of the project.
224 \item Design and management of a publicly available web-site that includes
225       descriptions of the main project results and allows the download of
226       all the software and publications developed in \cerco. The web-site will
227       be managed as a Wiki to maximise interaction with the community of
228       users and researchers interested in the project.
229 \item Press conferences and press releases describing the advancement and
230       main results of the project, so to reach and make the public aware of
231       both the short-term and long-term impact of the project results.
232 \item Dissemination of project objectives and results to members of
233       European or national level projects having \cerco{} members as
234       participants.
237\section{Description of the Dissemination Plan}
238\subsection{Web presence and information exchange}
239The website of the \cerco{} project is
241and it is made of a combination of a private and a public Wiki.
242The Wiki will progressively include:
244 \item A general introduction to the project: the objectives, the expected
245      results, the milestones, the detailed description of the consortium and
246      its coordinates within the Seventh Framework Programme.
247 \item The list of events taking place in the context of the project: meetings,
248      conferences, workshops, and their availability to the public.
249 \item Publications originated from the project, both in the scientific community and in the general press.
250 \item A number of relevant links: other projects, institutions and companies
251      that are related to \cerco.
252 \item A public section containing the public deliverables, comprising the
253       open source software developed in \cerco. In order to make a first
254       trial of the software as simple as possible for interested users,
255       we plan to provide packages for some common Linux distributions and
256       a Live CD for non Linux users.
257 \item A private section containing the remaining deliverables and other
258       documents for the European Commission.
259 \item A private section containing contact details, mailing lists archives,
260       details about the meetings (slides, notes and so on) and other
261       temporary technical information needed by the consortium.
264    Besides for the website, communication and information exchange among
265the members of the project is enforced via a carefully organized and maintained central repository and a number of dynamically created mailing lists.
267Ad-hoc advertisement of \cerco{} to the interested research communities will
268also be achieved by advertisements sent to the mailing lists of the projects,
269as well as advertisement of open job positions.
271\subsection{Project Workshops and Conferences, Lectures, Tutorials}
272Two Project Workshops will be organized every year.
273They will consist in a public and a private chapter and we will invite as
274guests a small number or international researchers who are working on related
275problems. We will try to colocate later workshops with international events
276to improve visibility of the project. During the third year we plan as well to
277organize two separate additional events targeted to the scientific community
278and to potential industrial stakeholders.
280Moreover, we aim to present our work at international conferences and
281forums on interactive and automatic theorem proving, resource aware computing,
282invariant generation, formal methods and reactive computing. In accordance
283with the character of the corresponding meeting, the presentation of \cerco{}
284may be part of a more comprehensive presentation, it may get a presentation of
285its own, or even only special aspects of \cerco{} may be addressed by a talk.
286In the latter case some member of the group caring about the relative task
287or work-package may be the most suitable person to give the talk. Talks at
288larger conferences should be accompanied by papers on \cerco{} in the corresponding proceedings.
291We aim to publish the results obtained in \cerco{} in the proceedings
292of international events and in international journals. The list of journals
293that publish papers related to the topics studied in \cerco{} comprises and
294it is not limited to the following ones:
297 \item Journal of Automated Reasoning
298 \item Journal of Formalized Reasoning
299 \item Information and Computation
300 \item Higher-Order and Symbolic Computation
301 \item Communications of the ACM
302 \item Science of computer programming
305Many international conferences and workshops deal with compilation,
306formal reasonings and resource analysis. Some of the most important are
310 \item Principles of Programming Languages (POPL)
311 \item Interactive Theorem Proving (ITP, ex TPHOLs)
312 \item Logic for Programming, Artificial Intelligence and Reasoning (LPAR)
313 \item Compiler Construction (CC)
314 \item International Symposium on Formal Methods (FM)
315 \item Symposium on Programming Languages and Reasoning (APLAS)
316 %\item Types for Proofs and Programs (TYPEs)
321This 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.
323\subsubsection{National/Local Projects and Research Groups}
325The following national/local projects and research groups are the most direct
326interlocutors for \cerco.
329 \item CompCert \url{}, the most advanced, closed
330       source project on the development of a certified compiler for a subset
331       of C, and a natural source of inspiration and competitor for \cerco.
332 \item Frama-C \url{}, an extensible and collaborative
333       platform dedicated to source-code analysis of C software. It is a
334       natural candidate for a technological integration with the \cerco{}
335       compiler in order to provide high-level reasoning tools on the
336       intentional properties of C programs.
337 \item AbsInt \url{} is a privately-held company located
338       in Saarbruecken, Germany, that participated to several EU projects and
339       has a good record of collaboration with the scientific community. It
340       develops advanced development tools for embedded systems, and tools for
341       validation, verification and certification of safety-critical software.
344\subsubsection{EU Projects}
346This is a selection of EU projects (mainly from FP7) dealing with embedded or,
347more generally, resource constrained systems.
350\item ARTEMIS: European Technology Platform/Joint Technology Initiative on
351      Advanced Research \& Technology for Embedded Intelligence and Systems
352\item Embounded: FP6 Strep on Automatic Analysis of Bounded Resources for Embedded Systems.
353\item ARTISTDesign: FP7 Network of Excellence on Design of Embedded Systems
354\item MNEMEE : FP7 Collaborative Project on Memory management technology for adaptive and efficient design of embedded systems. Jan 2008 -- Dec 2010.
355\item INTERESTED: FP7 Collaborative Project on Interoperable embedded systems Tool-chain for enhanced rapid design, prototyping and code generation. Jan 2008 -- Dec 2010.
356\item PREDATOR : FP7 Collaborative Project on Design for predictability and efficiency. Feb 2008 -- Jan 2011.
357\item QUASIMODO : FP7 Collaborative Project on Quantitative system properties in model-driven design of embedded systems. Jan 2008 -- Dec 2010.
360\section{Description of the Use Plan (by result)}\label{byresult}
362In this section, we describe the expected project results that are released
363in correspondence with project milestones and that have potential
364for exploitation.
366\subsection{Untrusted cost-annotating compiler}
367\textbf{Delivery date:} January 2011\\
369The untrusted cost-annotating compiler will be a functional compiler from
370a large subset of C to some assembly language. It will already trace the
371evolution of selected high-level code fragments in order to relate them to
372low level code fragments and it will manifest cost annotations in the source
374\textbf{Target communities:} compiler developers; developers of code invariant
375generators; developers of tools for cache behaviour prediction and general
376analysis of assembly code.\\
378Compiler developers will be interested by the techniques used to trace evelution
379of code fragments during compilation. They should also be interested in
380enhanching the proposed techniques to address more optimizations.
382Developers of code invariant generators will be able to apply and extend their
383own techniques to deal with exact execution time by considering cost annotations
384during the invariant generation phase.
386Developers of tools for cache behaviour prediction and general analysis of
387assembly code should be particularly interested since our approach allows to
388reflect on the source code their own analysis performed on low level target
392\textbf{Dissemination:} Information dissemination on this activity will be done
393on the general project level, but will also try to target specific communities
394by targeted presentations/participation to relative conferences or meetings.
395In particular we plan to invite selected members of those communities to the
396first annual \cerco{} meeting to advertise the project results and foster
397potential collaborations.
399\subsection{Untrusted CerCo compiler}
400\textbf{Delivery date:} January 2012\\
402The CerCo compiler will be a re-implementation of the untrusted cost-annotating
403compiler in the variant of the Calculus of (Co)Inductive Constructions
404implemented by Matita, ready to be certified. Moreover, it will enhance the
405previous prototype by integrating a new layer for the management of cost
406annotations (produced by the compiler) and the complexity assertions (added
407by the user or synthesized automatically by abstract interpretation algorithms)
408in order to produce the right complexity obligations, that is the goal to be
409proved in order to check the correctness of the assertions.\\
410\textbf{Target communities:} the interactive theorem proving community;
411developers of code invariant generators; the abstract interpretation
412community; end users.\\
414The interactive theorem proving community will benefit from an executable
415specification of a realistic compiler for C written in
416the Calculus of (Co)Inductive Constructions. However, at this stage the
417main benefit for the community will be a project by-product, which is
418a low level executable semantics (an interpreter) for some
419target machine and for several intermediate languages, that could easily be
420reused in other formalizations and translated to other interactive theorem
423Developers of code invariant generators and the abstract interpretation
424community should be interested in the new layer of management of cost
425annotations and complexity assertions in order to interface their techniques on
426top of it or to propose alternative management approaches. The prototype could
427also be used as a test-bench generator for their techniques.
429Starting with the release of the prototype we will begin to contact potential
430end users, i.e. developers of time critical software, in order to attract
431feedback and to ensure that the final outcome fulfil actual requirements of
432the targeted exploitation community.
435\textbf{Dissemination:} Information dissemination on this activity will be done
436on the general project level, with particular attention to the interactive
437theorem proving community. We will continue the practice of inviting
438selected members of the interested communities to the
439annual \cerco{} meetings to advertise the project results and foster
440potential collaborations. Moreover we will gradually enlarge the scope of the
441dissemination activity from developers and researchers in formal methods to
442the wider audience of users of compilers that are potentially interested in
443exact execution time, even if at this stage we do not expect
444applications of the prototype to realistic programs.
446\subsection{Trusted CerCo compiler}
447\textbf{Delivery date:} January 2013\\
449The trusted CerCo compiler is the final prototype of \cerco{} and it is
450composed of several components
452 \item a proof of correctness in Matita of the
453compliance of the compiler, described as preservation of both the extensional
454and intensional behaviour of the program;
455 \item an extension of the interactive
456theorem prover Matita with ad-hoc tactics and mechanism targeted towards the
457progressive automation --- either in the small or in the large --- of complexity
459 \item an extensive use case dedicated to the automatic generation of
460cost invariants for the C code generated by a synchronous language compiler.
461The functionalities developed in the use case will be tested to compute
462certified reaction time bounds for significant examples of synchronous
465\textbf{Target communities:} the interactive and automatic theorem proving
466community; developers of code invariant generators; end users, in particular
467synchronous languages programmers.\\
469The interactive theorem proving community will benefit from the first fully
470open source proof of correctness of a realistic compiler for C written in
471the Calculus of (Co)Inductive Constructions and for a new technique to formally
472verify preservation of intentional properties without loosing precision.
473Developers of both interactive and automatic theorem provers will be interested
474in testing and enhancing their tecniques when applied to automation of
475complexity proofs.
477The final prototype of the \cerco{} project is supposed to be the first
478realistic milestone towards the formal certification of exact execution time
479(or exact reaction time) for real time or synchronous programs and thus
480it is meant to attract interest from end users. In particular, we will be
481looking for feedback on the applicability of the proposed technique and we
482will target in particular the sub-community of syncronous programmers.
485\textbf{Dissemination:} We will increase our dissemination activity during the
486last year of the project, in particular organizing separate events targeted to
487the scientific community and to the potential industrial stakeholders. We will
488also improve accessibility and visibility of the \cerco{} compiler by developing
489packages for Linux distributions and Live CDs for non-Linux users.
492%\bibitem{matita} The Interactive Theorem Prover Matita,
493% \url{}
494%\bibitem{subversion}The Version Control System Subversion,
495% \url{}
496%\bibitem{trac}The Integrated SCM \& Project Management tool Trac,
497% \url{}
Note: See TracBrowser for help on using the repository browser.