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

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

finished touching up report's English

File size: 28.3 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 signed a Consortium Agreement before the start of the
190project, legally confirming the principles of consortium management and
191mutually agreeing the precise relationship between the partners and their
192respective responsibilities for the duration of the work. In particular, the
193agreement includes specific arrangements with regard to intellectual property
194rights, to be applied amongst the participants and their affiliates, in compliance
195with the general arrangements stipulated in the contract.
196It thus specifies the rules for dissemination and use (confidentiality,
197ownership of results, patent rights, exploitation of results, and protection and
198dissemination of knowledge), as well as financial and legal provisions.
199A peculiarity of \cerco{} is that we are self-constrained to release open-source
200software only, which is also manifest in our prototypes that will all be made
201publicly accessible, nor did we identify any background to be protected.
203\subsection{Approach to Dissemination and Use}
204The \cerco{} project represents an unprecedented effort to create a verified
205chain of trust for intentional program properties during compilation,
206and we thus expect that, in the short term, it will generate a significant
207amount of interest in academia and, in the longer term, a significant amount of
208interest in industry, as well.
210Dissemination and use of foreground will have a high priority that will be
211intensified towards the end of the project and whose target will progressively
212shift from academia to potential end users.
213Work package 6 will be devoted to all activities relevant to accomplishing this
216We have planned appropriate measures to ensure an effective and timely
217dissemination of the project results to potential users, both at the European
218level and worldwide. Since the research started in \cerco{} is of the
219long term kind, the main target of dissemination will be research institutions
220that may immediately benefit from our results, and possibly take over the
221research effort after the termination of the \cerco{} project, to achieve long
222term results. We will also target industry by means of specific dissemination
223actions towards the end of the project in order to advertise our results, and to
224ensure that the final outcome will fulfil the specific requirements of the
225industrial community.
227Dissemination will be carried out by a variety of means:
229 \item Talks at relevant international conferences, events and forums (both
230       presenting the technical achievements and introducing at a high level
231       the project’s objectives and results).
232 \item Publication of papers in proceedings of international conferences and
233       events, as well as in international scientific journals.
234 \item Organisation of meetings on project-related topics,
235       including `project workshops' where attendance of external experts
236       and professionals is based on invitation.
237 \item Organisation of at least one special event targeted at the scientific
238       community, in the form of an open workshop, possibly affiliated to a
239       major conference, or in the form of courses given at summer schools
240       or equivalent teaching events targeted to PhD students.
241 \item Organisation of at least one special event targeted at potential
242       industrial stakeholders, in the form of a dissemination meeting to
243       be hold during the last year of the project.
244 \item Design and management of a publicly available website that includes
245       descriptions of the main project results and allows the download of
246       all the software and publications developed in \cerco. The web-site will
247       be managed as a Wiki to maximise interaction with the community of
248       users and researchers interested in the project.
249 \item Press conferences and press releases describing the advancement and
250       main results of the project, so as to reach and make the public aware of
251       both the short-term and long-term impact of the project results.
252 \item Dissemination of project objectives and results to members of
253       European or national level projects having \cerco{} members as
254       participants.
257\section{Description of the Dissemination Plan}
258\subsection{Web presence and information exchange}
259The website of the \cerco{} project is
261The website combines a private and public Wiki.
262The Wiki will progressively include:
264 \item A general introduction to the project: the objectives, the expected
265      results, the milestones, the detailed description of the consortium and
266      its position within the Seventh Framework Programme.
267 \item The list of events taking place in the context of the project: meetings,
268      conferences, workshops, and their availability to the public.
269 \item Publications originating with the project, both in the scientific
270       community and in the general press.
271 \item A number of relevant links: other projects, institutions and companies
272      that are related to \cerco.
273 \item A public section containing the public deliverables, comprising the
274       open source software developed in \cerco. In order to make a first
275       trial of the software as simple as possible for interested users,
276       we plan to provide packages for some common Linux distributions and
277       a Live CD for non Linux users.
278 \item A private section containing the remaining deliverables and other
279       documents for the European Commission.
280 \item A private section containing contact details, mailing lists archives,
281       details about meetings held (slides, notes and so on) and other
282       temporary technical information needed by the consortium.
285Besides the website, communication and information exchange amongst the members
286of the project is enforced via a carefully organized and maintained central
287repository and a number of dynamically created mailing lists.
289\emph{Ad hoc} advertisement of \cerco{} to the interested research communities will
290also be achieved by advertisements sent to the mailing lists of the projects,
291as well as advertisement of open job positions.
293\subsection{Project Workshops and Conferences, Lectures, Tutorials}
294Two Project Workshops will be organized every year.
295They will consist of a public and a private chapter and we will invite as
296guests a small number or international researchers who are working on related
297problems. We will try to co-locate later workshops with international events
298in order to improve visibility of the project. During the third year we also
299plan to organise two separate additional events targeted at the scientific
300community and to potential industrial stakeholders.
302Moreover, we aim to present our work at international conferences and
303forums on interactive and automatic theorem proving, resource aware computing,
304invariant generation, formal methods and reactive computing. In accordance
305with the character of the corresponding meeting, the presentation of \cerco{}
306may be part of a more comprehensive presentation, it may get a presentation of
307its own, or even only special aspects of \cerco{} may be addressed by a talk.
308In the latter case some member of the group with expertise in the respective task
309or work-package may be the most suitable person to give the talk. Talks at
310larger conferences should be accompanied by papers on \cerco{} in the
311corresponding proceedings.
314We aim to publish the results obtained in \cerco{} in the proceedings
315of international events and in international journals. The list of journals
316that publish papers related to the topics studied in \cerco{} comprises, but
317it is not limited to, the following ones:
320 \item Journal of Automated Reasoning
321 \item Journal of Formalized Reasoning
322 \item Information and Computation
323 \item Higher-Order and Symbolic Computation
324 \item Communications of the ACM
325 \item Science of computer programming
328Many international conferences and workshops deal with compilation,
329formal reasonings and resource analysis. Some of the most important are
333 \item Principles of Programming Languages (POPL)
334 \item Interactive Theorem Proving (ITP, ex TPHOLs)
335 \item Logic for Programming, Artificial Intelligence and Reasoning (LPAR)
336 \item Compiler Construction (CC)
337 \item International Symposium on Formal Methods (FM)
338 \item Symposium on Programming Languages and Reasoning (APLAS)
339 %\item Types for Proofs and Programs (TYPEs)
344This section indicates some projects and organisations relevant to the ongoing
345work (at world-wide, European or national level) and with which information
346exchange may be beneficial.
348\subsubsection{National/Local Projects and Research Groups}
350The following national/local projects and research groups are the most direct
351interlocutors for \cerco.
354 \item CompCert \url{}: the most advanced, closed
355       source project on the development of a certified compiler for a subset
356       of C, and a natural source of inspiration (and competitor) for \cerco.
357 \item Frama-C \url{}: an extensible and collaborative
358       platform dedicated to source-code analysis of C software. It is a
359       natural candidate for a technological integration with the \cerco{}
360       compiler, in order to provide high-level reasoning tools on the
361       intentional properties of C programs.
362 \item AbsInt \url{}: a private company located
363       in Saarbruecken, Germany, that participated in several EU projects and
364       has a good record of collaboration with the scientific community. It
365       develops advanced development tools for embedded systems, and tools for
366       validation, verification and certification of safety-critical software.
369\subsubsection{EU Projects}
371This is a selection of EU projects (mainly from FP7) dealing with embedded or,
372more generally, resource constrained systems.
375\item ARTEMIS: European Technology Platform/Joint Technology Initiative on
376      Advanced Research \& Technology for Embedded Intelligence and Systems
377\item Embounded: FP6 Strep on Automatic Analysis of Bounded Resources for Embedded Systems.
378\item ARTISTDesign: FP7 Network of Excellence on Design of Embedded Systems
379\item MNEMEE : FP7 Collaborative Project on Memory management technology for adaptive and efficient design of embedded systems. Jan 2008--Dec 2010.
380\item INTERESTED: FP7 Collaborative Project on Interoperable embedded systems Tool-chain for enhanced rapid design, prototyping and code generation. Jan 2008--Dec 2010.
381\item PREDATOR : FP7 Collaborative Project on Design for predictability and efficiency. Feb 2008--Jan 2011.
382\item QUASIMODO : FP7 Collaborative Project on Quantitative system properties in model-driven design of embedded systems. Jan 2008--Dec 2010.
385\section{Description of the Use Plan (by result)}\label{byresult}
387In this section, we describe the expected project results that are released
388in correspondence with project milestones and that have potential
389for exploitation.
391\subsection{Untrusted cost-annotating compiler}
392\textbf{Delivery date:} January 2011\\
394The untrusted cost-annotating compiler will be a functional compiler from
395a large subset of C to some assembly language. It will already trace the
396evolution of selected high-level code fragments in order to relate them to
397low level code fragments, and it will manifest cost annotations in the source
399\textbf{Target communities:} compiler developers; developers of code invariant
400generators; developers of tools for cache behaviour prediction and general
401analysis of assembly code.\\
403Compiler developers will be interested in the techniques used to trace evolution
404of code fragments during compilation. They should also be interested in
405suggesting enhancements to the proposed technique, in order to address more
408Developers of code invariant generators will be able to apply and extend their
409own techniques to deal with exact execution time by considering cost annotations
410during the invariant generation phase.
412Developers of tools for cache behaviour prediction and general analysis of
413assembly code should be particularly interested since our approach allows to
414reflect at the source code level their own analyses performed on low-level target
418\textbf{Dissemination:} Information dissemination for this activity will be done
419at the general project level, but will also try to target specific communities
420by targeted presentations/participation at relative conferences or meetings.
421In particular we plan to invite selected members of those communities to the
422first annual \cerco{} meeting to advertise the project results and foster
423potential collaborations.
425\subsection{Untrusted CerCo compiler}
426\textbf{Delivery date:} January 2012\\
428The CerCo compiler will be a re-implementation of the untrusted cost-annotating
429compiler in the variant of the Calculus of (Co)Inductive Constructions
430implemented by Matita, ready to be certified. Moreover, it will enhance the
431previous prototype by integrating a new layer for the management of cost
432annotations (produced by the compiler) and the complexity assertions (added
433by the user or synthesized automatically by abstract interpretation algorithms)
434in order to produce the right complexity obligations, that is, the goal to be
435proved in order to check the correctness of the assertions.\\
436\textbf{Target communities:} the interactive theorem proving community;
437developers of code invariant generators; the abstract interpretation
438community; end users.\\
440The interactive theorem proving community will benefit from an executable
441specification of a realistic compiler for C written in
442the Calculus of (Co)Inductive Constructions. However, at this stage the
443main benefit for the community will be a project by-product, which is
444a low level executable semantics (an interpreter) for some
445target machine and for several intermediate languages, that could easily be
446reused in other formalizations and translated to other interactive theorem
449Developers of code invariant generators and the abstract interpretation
450community should be interested in the new layer of management of cost
451annotations and complexity assertions in order to interface their techniques on
452top of it or to propose alternative management approaches. The prototype could
453also be used as a test-bench generator for their techniques.
455Starting with the release of the prototype we will begin to contact potential
456end users, i.e. developers of time critical software, in order to attract
457feedback and to ensure that the final outcome will fulfil the specific
458requirements of the targeted exploitation community.
461\textbf{Dissemination:} Information dissemination for this activity will be done
462at the general project level, with particular attention to the interactive
463theorem proving community. We will continue the practice of inviting
464selected members of the interested communities to the
465annual \cerco{} meetings in order to advertise the project results and foster
466potential collaborations. Moreover we will gradually enlarge the scope of the
467dissemination activity from developers and researchers in formal methods to
468the wider audience of users of compilers that are potentially interested in
469exact execution time, even if at this stage we do not expect the prototype
470compiler to apply to realistic programs.
472\subsection{Trusted CerCo compiler}
473\textbf{Delivery date:} January 2013\\
475The trusted CerCo compiler is the final prototype of \cerco{} and it is
476composed of several components:
478 \item a proof of correctness in Matita of the
479compliance of the compiler, described as preservation of both the extensional
480and intensional behaviour of the program;
481 \item an extension of the interactive
482theorem prover Matita with \emph{ad hoc} tactics and mechanisms targeted toward the
483progressive automation---either in the small or in the large---of complexity
485 \item an extensive use case dedicated to the automatic generation of
486cost invariants for the C code generated by a synchronous language compiler.
487The functionalities developed in the use case will be tested to compute
488certified reaction time bounds for significant examples of synchronous
491\textbf{Target communities:} the interactive and automatic theorem proving
492community; developers of code invariant generators; end users, in particular
493synchronous languages programmers.\\
495The interactive theorem proving community will benefit from the first fully
496open source proof of correctness of a realistic compiler for C written in
497the Calculus of (Co)Inductive Constructions, and for a new technique for formally
498verifying preservation of intentional properties without losing precision.
499Developers of both interactive and automatic theorem provers will be interested
500in testing and enhancing their techniques when applied to automation of
501complexity proofs.
503The final prototype of the \cerco{} project is supposed to be the first
504realistic milestone towards the formal certification of exact execution time
505(or exact reaction time) for real time or synchronous programs and thus
506it is meant to attract interest from end users. In particular, we will be
507looking for feedback on the applicability of the proposed technique, and we
508will target in particular the sub-community of synchronous programmers.
511\textbf{Dissemination:} We will increase our dissemination activity during the
512final year of the project, in particular organizing separate events targeted at
513the scientific community and to potential industrial stakeholders. We will
514also improve accessibility and visibility of the \cerco{} compiler by developing
515packages for Linux distributions, and Live CDs for non-Linux users.
518%\bibitem{matita} The Interactive Theorem Prover Matita,
519% \url{}
520%\bibitem{subversion}The Version Control System Subversion,
521% \url{}
522%\bibitem{trac}The Integrated SCM \& Project Management tool Trac,
523% \url{}
Note: See TracBrowser for help on using the repository browser.