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

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

First draft.

File size: 25.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 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.
153milestone name & due at month \\ \hline
154Untrusted cost-annotating compiler & 12 \\
155Untrusted CerCo compiler & 24 \\
156Trusted CerCo compiler & 36 \\
160\subsection{Management of knowledge and intellectual property}
161All project partners have signed a Consortium Agreement before the start
162of the project, setting the principles of the consortium management and
163placing the relationship between the partners and their responsibilities on
164a legal basis for the duration of the work. In particular, the agreement
165includes specific arrangements concerning intellectual property rights to be
166 applied among the participants and their affiliates, in compliance with the
167general arrangements stipulated in the contract.
168It thus specifies the rules
169for dissemination and use (confidentiality, ownership of results, patent rights,
170exploitation of results, protection and dissemination of knowledge), as well
171as financial and legal provisions.
172A peculiarity of \cerco{}
173is that we self-constrained to release open source software only, which is
174also manifest in our prototypes that will all be public, and that we did not
175identify any background to be protected.
177\subsection{Approach to Dissemination and Use}
178The \cerco{} project represents an unprecedented effort to create a verified
179chain of trust for intentional program properties during compilation,
180and we thus expect that it will generate in the short term a large interest in
181academia and in a longer term also a significant one in industry.
183Dissemination and use of foreground will have a high priority that will be
184intensified towards the end of the project and whose target will progressively
185shift from academia to potential end users.
186Work package 6 will be devoted to all the activities relevant to accomplishing this task.
188    We have planned appropriate measures to ensure an effective and
189timely dissemination of the project results to potential users, both at the European level and worldwide. Since the research started in \cerco{} is of the
190long term kind, the main target of the dissemination activity will be research
191institutions that can immediately benefit from our results and that should take
192over the research effort after the end of \cerco{} to achieve the long terms
193results. We will also target industry by means of specific dissemination actions
194towards the end of the project in order to advertise our results and to ensure
195that the final outcome fulfil actual requirements of the industrial community.
197Dissemination will be carried out by a variety of means:
199 \item Talks at relevant international conferences, events and forums (both
200       presenting the technical achievements and introducing at a high level
201       the project’s objectives and results).
202 \item Publication of papers in proceedings of international conferences and
203       events, as well as in international scientific journals.
204 \item Organization of meetings on project-related topics,
205       including ``project workshops'' where attendance of external experts
206       and professionals is based on invitation.
207 \item Organization of at least one special event targeted to the scientific
208       community, in the form of an open workshop, possibly affiliated to a
209       major conference, or in the form of courses given at summer schools
210       or equivalent teaching events targeted to Ph.D. students.
211 \item Organization of at least one special even targeted to potential
212       industrial stakeholders, in the form of a dissemination meeting to
213       be hold during the last year of the project.
214 \item Design and management of a publicly available web-site that includes
215       descriptions of the main project results and allows the download of
216       all the software and publications developed in \cerco. The web-site will
217       be managed as a Wiki to maximise interaction with the community of
218       users and researchers interested in the project.
219 \item Press conferences and press releases describing the advancement and
220       main results of the project, so to reach and make the public aware of
221       both the short-term and long-term impact of the project results.
222 \item Dissemination of project objectives and results to members of
223       European or national level projects having \cerco{} members as
224       participants.
227\section{Description of the Dissemination Plan}
228\subsection{Web presence and information exchange}
229The website of the \cerco{} project is
231and it is made of a combination of a private and a public Wiki.
232The Wiki will progressively include:
234 \item A general introduction to the project: the objectives, the expected
235      results, the milestones, the detailed description of the consortium and
236      its coordinates within the Seventh Framework Programme.
237 \item The list of events taking place in the context of the project: meetings,
238      conferences, workshops, and their availability to the public.
239 \item Publications originated from the project, both in the scientific community and in the general press.
240 \item A number of relevant links: other projects, institutions and companies
241      that are related to \cerco.
242 \item A public section containing the public deliverables, comprising the
243       open source software developed in \cerco. In order to make a first
244       trial of the software as simple as possible for interested users,
245       we plan to provide packages for some common Linux distributions and
246       a Live CD for non Linux users.
247 \item A private section containing the remaining deliverables and other
248       documents for the European Commission.
249 \item A private section containing contact details, mailing lists archives,
250       details about the meetings (slides, notes and so on) and other
251       temporary technical information needed by the consortium.
254    Besides for the website, communication and information exchange among
255the members of the project is enforced via a carefully organized and maintained central repository and a number of dynamically created mailing lists.
257Ad-hoc advertisement of \cerco{} to the interested research communities will
258also be achieved by advertisements sent to the mailing lists of the projects,
259as well as advertisement of open job positions.
261\subsection{Project Workshops and Conferences, Lectures, Tutorials}
262Two Project Workshops will be organized every year.
263They will consist in a public and a private chapter and we will invite as
264guests a small number or international researchers who are working on related
265problems. We will try to colocate later workshops with international events
266to improve visibility of the project. During the third year we plan as well to
267organize two separate additional events targeted to the scientific community
268and to potential industrial stakeholders.
270Moreover, we aim to present our work at international conferences and
271forums on interactive and automatic theorem proving, resource aware computing,
272invariant generation, formal methods and reactive computing. In accordance
273with the character of the corresponding meeting, the presentation of \cerco{}
274may be part of a more comprehensive presentation, it may get a presentation of
275its own, or even only special aspects of \cerco{} may be addressed by a talk.
276In the latter case some member of the group caring about the relative task
277or work-package may be the most suitable person to give the talk. Talks at
278larger conferences should be accompanied by papers on \cerco{} in the corresponding proceedings.
281We aim to publish the results obtained in \cerco{} in the proceedings
282of international events and in international journals. The list of journals
283that publish papers related to the topics studied in \cerco{} comprises and
284it is not limited to the following ones:
287 \item Journal of Automated Reasoning
288 \item Journal of Formalized Reasoning
289 \item Information and Computation
290 \item Higher-Order and Symbolic Computation
291 \item Communications of the ACM
292 \item Science of computer programming
295Many international conferences and workshops deal with compilation,
296formal reasonings and resource analysis. Some of the most important are
300 \item Principles of Programming Languages (POPL)
301 \item Interactive Theorem Proving (ITP, ex TPHOLs)
302 \item Logic for Programming, Artificial Intelligence and Reasoning (LPAR)
303 \item Compiler Construction (CC)
304 \item International Symposium on Formal Methods (FM)
305 \item Symposium on Programming Languages and Reasoning (APLAS)
306 %\item Types for Proofs and Programs (TYPEs)
311This 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.
315%• ARTIST2: FP6 Network of Excellence on Embedded Systems Design.
316%  Sep 2004 – Aug 2008,
317%• ARTISTDesign: FP7 Network of Excellence on Design of Embedded Systems.
318%  Jan 2008 – Dec 2011, project/ArtistDesign.
319%• DEPLOY: Industrial deployment of system engineering methods pro-
320%  viding high dependability and productivity. FP7 project, Feb 2008 –
321%  Jan 2012,
322%• MASTER: Managing Assurance, Security and Trust for sERvices. FP7
323%  project, Feb 2008 – Jan 2011,
324%  php.
325%• SENSORIA: Software Engineering for Service-Oriented Overlay Computers,
326%  FP6 project, Sep 2005 – Aug 2009, http://www.sensoria-ist.
327%• SERENITY: System Engineering for Security and Dependability. FP6
328%  project, Jan 2006 – Dec 2008,
330\section{Description of the Use Plan (by result)}\label{byresult}
332In this section, we describe the expected project results that are released
333in correspondence with project milestones and that have potential
334for exploitation.
336\subsection{Untrusted cost-annotating compiler}
337\textbf{Delivery date:} January 2011\\
339The untrusted cost-annotating compiler will be a functional compiler from
340a large subset of C to some assembly language. It will already trace the
341evolution of selected high-level code fragments in order to relate them to
342low level code fragments and it will manifest cost annotations in the source
344\textbf{Target communities:} compiler developers; developers of code invariant
345generators; developers of tools for cache behaviour prediction and general
346analysis of assembly code.\\
348Compiler developers will be interested by the techniques used to trace evelution
349of code fragments during compilation. They should also be interested in
350enhanching the proposed techniques to address more optimizations.
352Developers of code invariant generators will be able to apply and extend their
353own techniques to deal with exact execution time by considering cost annotations
354during the invariant generation phase.
356Developers of tools for cache behaviour prediction and general analysis of
357assembly code should be particularly interested since our approach allows to
358reflect on the source code their own analysis performed on low level target
362\textbf{Dissemination:} Information dissemination on this activity will be done
363on the general project level, but will also try to target specific communities
364by targeted presentations/participation to relative conferences or meetings.
365In particular we plan to invite selected members of those communities to the
366first annual \cerco{} meeting to advertise the project results and foster
367potential collaborations.
369\subsection{Untrusted CerCo compiler}
370\textbf{Delivery date:} January 2012\\
372The CerCo compiler will be a re-implementation of the untrusted cost-annotating
373compiler in the variant of the Calculus of (Co)Inductive Constructions
374implemented by Matita, ready to be certified. Moreover, it will enhance the
375previous prototype by integrating a new layer for the management of cost
376annotations (produced by the compiler) and the complexity assertions (added
377by the user or synthesized automatically by abstract interpretation algorithms)
378in order to produce the right complexity obligations, that is the goal to be
379proved in order to check the correctness of the assertions.\\
380\textbf{Target communities:} the interactive theorem proving community;
381developers of code invariant generators; the abstract interpretation
382community; end users.\\
384The interactive theorem proving community will benefit from an executable
385specification of a realistic compiler for C written in
386the Calculus of (Co)Inductive Constructions. However, at this stage the
387main benefit for the community will be a project by-product, which is
388a low level executable semantics (an interpreter) for some
389target machine and for several intermediate languages, that could easily be
390reused in other formalizations and translated to other interactive theorem
393Developers of code invariant generators and the abstract interpretation
394community should be interested in the new layer of management of cost
395annotations and complexity assertions in order to interface their techniques on
396top of it or to propose alternative management approaches. The prototype could
397also be used as a test-bench generator for their techniques.
399Starting with the release of the prototype we will begin to contact potential
400end users, i.e. developers of time critical software, in order to attract
401feedback and to ensure that the final outcome fulfil actual requirements of
402the targeted exploitation community.
405\textbf{Dissemination:} Information dissemination on this activity will be done
406on the general project level, with particular attention to the interactive
407theorem proving community. We will continue the practice of inviting
408selected members of the interested communities to the
409annual \cerco{} meetings to advertise the project results and foster
410potential collaborations. Moreover we will gradually enlarge the scope of the
411dissemination activity from developers and researchers in formal methods to
412the wider audience of users of compilers that are potentially interested in
413exact execution time, even if at this stage we do not expect
414applications of the prototype to realistic programs.
416\subsection{Trusted CerCo compiler}
417\textbf{Delivery date:} January 2013\\
419The trusted CerCo compiler is the final prototype of \cerco{} and it is
420composed of several components
422 \item a proof of correctness in Matita of the
423compliance of the compiler, described as preservation of both the extensional
424and intensional behaviour of the program;
425 \item an extension of the interactive
426theorem prover Matita with ad-hoc tactics and mechanism targeted towards the
427progressive automation --- either in the small or in the large --- of complexity
429 \item an extensive use case dedicated to the automatic generation of
430cost invariants for the C code generated by a synchronous language compiler.
431The functionalities developed in the use case will be tested to compute
432certified reaction time bounds for significant examples of synchronous
435\textbf{Target communities:} the interactive and automatic theorem proving
436community; developers of code invariant generators; end users, in particular
437synchronous languages programmers.\\
439The interactive theorem proving community will benefit from the first fully
440open source proof of correctness of a realistic compiler for C written in
441the Calculus of (Co)Inductive Constructions and for a new technique to formally
442verify preservation of intentional properties without loosing precision.
443Developers of both interactive and automatic theorem provers will be interested
444in testing and enhancing their tecniques when applied to automation of
445complexity proofs.
447The final prototype of the \cerco{} project is supposed to be the first
448realistic milestone towards the formal certification of exact execution time
449(or exact reaction time) for real time or synchronous programs and thus
450it is meant to attract interest from end users. In particular, we will be
451looking for feedback on the applicability of the proposed technique and we
452will target in particular the sub-community of syncronous programmers.
455\textbf{Dissemination:} We will increase our dissemination activity during the
456last year of the project, in particular organizing separate events targeted to
457the scientific community and to the potential industrial stakeholders. We will
458also improve accessibility and visibility of the \cerco{} compiler by developing
459packages for Linux distributions and Live CDs for non-Linux users.
462%\bibitem{matita} The Interactive Theorem Prover Matita,
463% \url{}
464%\bibitem{subversion}The Version Control System Subversion,
465% \url{}
466%\bibitem{trac}The Integrated SCM \& Project Management tool Trac,
467% \url{}
Note: See TracBrowser for help on using the repository browser.