# Changeset 48 for Deliverables

Ignore:
Timestamp:
Sep 9, 2010, 11:47:42 AM (10 years ago)
Message:

finished touching up report's English

File:
1 edited

### Legend:

Unmodified
 r47 \subsection{Management of knowledge and intellectual property} All project partners have signed a Consortium Agreement before the start of the project, setting the principles of the consortium management and placing the relationship between the partners and their responsibilities on a legal basis for the duration of the work. In particular, the agreement includes specific arrangements concerning intellectual property rights to be applied among the participants and their affiliates, in compliance with the general arrangements stipulated in the contract. It thus specifies the rules for dissemination and use (confidentiality, ownership of results, patent rights, exploitation of results, protection and dissemination of knowledge), as well as financial and legal provisions. A peculiarity of \cerco{} is that we self-constrained to release open source software only, which is also manifest in our prototypes that will all be public, and that we did not identify any background to be protected. All project partners signed a Consortium Agreement before the start of the project, legally confirming the principles of consortium management and mutually agreeing the precise relationship between the partners and their respective responsibilities for the duration of the work. In particular, the agreement includes specific arrangements with regard to intellectual property rights, to be applied amongst the participants and their affiliates, in compliance with the general arrangements stipulated in the contract. It thus specifies the rules for dissemination and use (confidentiality, ownership of results, patent rights, exploitation of results, and protection and dissemination of knowledge), as well as financial and legal provisions. A peculiarity of \cerco{} is that we are self-constrained to release open-source software only, which is also manifest in our prototypes that will all be made publicly accessible, nor did we identify any background to be protected. \subsection{Approach to Dissemination and Use} The \cerco{} project represents an unprecedented effort to create a verified chain of trust for intentional program properties during compilation, and we thus expect that it will generate in the short term a large interest in academia and in a longer term also a significant one in industry. and we thus expect that, in the short term, it will generate a significant amount of interest in academia and, in the longer term, a significant amount of interest in industry, as well. Dissemination and use of foreground will have a high priority that will be intensified towards the end of the project and whose target will progressively shift from academia to potential end users. Work package 6 will be devoted to all the activities relevant to accomplishing this task. We have planned appropriate measures to ensure an effective and timely dissemination of the project results to potential users, both at the European level and worldwide. Since the research started in \cerco{} is of the long term kind, the main target of the dissemination activity will be research institutions that can immediately benefit from our results and that should take over the research effort after the end of \cerco{} to achieve the long terms results. We will also target industry by means of specific dissemination actions towards the end of the project in order to advertise our results and to ensure that the final outcome fulfil actual requirements of the industrial community. Work package 6 will be devoted to all activities relevant to accomplishing this task. We have planned appropriate measures to ensure an effective and timely dissemination of the project results to potential users, both at the European level and worldwide. Since the research started in \cerco{} is of the long term kind, the main target of dissemination will be research institutions that may immediately benefit from our results, and possibly take over the research effort after the termination of the \cerco{} project, to achieve long term results. We will also target industry by means of specific dissemination actions towards the end of the project in order to advertise our results, and to ensure that the final outcome will fulfil the specific requirements of the industrial community. Dissemination will be carried out by a variety of means: \item Publication of papers in proceedings of international conferences and events, as well as in international scientific journals. \item Organization of meetings on project-related topics, including project workshops'' where attendance of external experts \item Organisation of meetings on project-related topics, including `project workshops' where attendance of external experts and professionals is based on invitation. \item Organization of at least one special event targeted to the scientific \item Organisation of at least one special event targeted at the scientific community, in the form of an open workshop, possibly affiliated to a major conference, or in the form of courses given at summer schools or equivalent teaching events targeted to Ph.D. students. \item Organization of at least one special even targeted to potential or equivalent teaching events targeted to PhD students. \item Organisation of at least one special event targeted at potential industrial stakeholders, in the form of a dissemination meeting to be hold during the last year of the project. \item Design and management of a publicly available web-site that includes \item Design and management of a publicly available website that includes descriptions of the main project results and allows the download of all the software and publications developed in \cerco. The web-site will users and researchers interested in the project. \item Press conferences and press releases describing the advancement and main results of the project, so to reach and make the public aware of main results of the project, so as to reach and make the public aware of both the short-term and long-term impact of the project results. \item Dissemination of project objectives and results to members of The website of the \cerco{} project is \begin{center}\url{cerco.cs.unibo.it}\end{center} and it is made of a combination of a private and a public Wiki. The website combines a private and public Wiki. The Wiki will progressively include: \begin{itemize} \item A general introduction to the project: the objectives, the expected results, the milestones, the detailed description of the consortium and its coordinates within the Seventh Framework Programme. its position within the Seventh Framework Programme. \item The list of events taking place in the context of the project: meetings, conferences, workshops, and their availability to the public. \item Publications originated from the project, both in the scientific community and in the general press. \item Publications originating with the project, both in the scientific community and in the general press. \item A number of relevant links: other projects, institutions and companies that are related to \cerco. documents for the European Commission. \item A private section containing contact details, mailing lists archives, details about the meetings (slides, notes and so on) and other details about meetings held (slides, notes and so on) and other temporary technical information needed by the consortium. \end{itemize} Besides for the website, communication and information exchange among the members of the project is enforced via a carefully organized and maintained central repository and a number of dynamically created mailing lists. Ad-hoc advertisement of \cerco{} to the interested research communities will Besides the website, communication and information exchange amongst the members of the project is enforced via a carefully organized and maintained central repository and a number of dynamically created mailing lists. \emph{Ad hoc} advertisement of \cerco{} to the interested research communities will also be achieved by advertisements sent to the mailing lists of the projects, as well as advertisement of open job positions. \subsection{Project Workshops and Conferences, Lectures, Tutorials} Two Project Workshops will be organized every year. They will consist in a public and a private chapter and we will invite as They will consist of a public and a private chapter and we will invite as guests a small number or international researchers who are working on related problems. We will try to co-locate later workshops with international events to improve visibility of the project. During the third year we plan as well to organize two separate additional events targeted to the scientific community and to potential industrial stakeholders. in order to improve visibility of the project. During the third year we also plan to organise two separate additional events targeted at the scientific community and to potential industrial stakeholders. Moreover, we aim to present our work at international conferences and may be part of a more comprehensive presentation, it may get a presentation of its own, or even only special aspects of \cerco{} may be addressed by a talk. In the latter case some member of the group caring about the relative task In the latter case some member of the group with expertise in the respective task or work-package may be the most suitable person to give the talk. Talks at larger conferences should be accompanied by papers on \cerco{} in the corresponding proceedings. larger conferences should be accompanied by papers on \cerco{} in the corresponding proceedings. \subsection{Publications} We aim to publish the results obtained in \cerco{} in the proceedings of international events and in international journals. The list of journals that publish papers related to the topics studied in \cerco{} comprises and it is not limited to the following ones: that publish papers related to the topics studied in \cerco{} comprises, but it is not limited to, the following ones: \begin{itemize} \subsection{Clustering} This 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. This section indicates some projects and organisations relevant to the ongoing work (at world-wide, European or national level) and with which information exchange may be beneficial. \subsubsection{National/Local Projects and Research Groups} \begin{itemize} \item CompCert \url{http://compcert.inria.fr}, the most advanced, closed \item CompCert \url{http://compcert.inria.fr}: the most advanced, closed source project on the development of a certified compiler for a subset of C, and a natural source of inspiration and competitor for \cerco. \item Frama-C \url{http://frama-c.com}, an extensible and collaborative of C, and a natural source of inspiration (and competitor) for \cerco. \item Frama-C \url{http://frama-c.com}: an extensible and collaborative platform dedicated to source-code analysis of C software. It is a natural candidate for a technological integration with the \cerco{} compiler in order to provide high-level reasoning tools on the compiler, in order to provide high-level reasoning tools on the intentional properties of C programs. \item AbsInt \url{http://absint.com} is a privately-held company located in Saarbruecken, Germany, that participated to several EU projects and \item AbsInt \url{http://absint.com}: a private company located in Saarbruecken, Germany, that participated in several EU projects and has a good record of collaboration with the scientific community. It develops advanced development tools for embedded systems, and tools for \item Embounded: FP6 Strep on Automatic Analysis of Bounded Resources for Embedded Systems. \item ARTISTDesign: FP7 Network of Excellence on Design of Embedded Systems \item MNEMEE : FP7 Collaborative Project on Memory management technology for adaptive and efficient design of embedded systems. Jan 2008 -- Dec 2010. \item INTERESTED: FP7 Collaborative Project on Interoperable embedded systems Tool-chain for enhanced rapid design, prototyping and code generation. Jan 2008 -- Dec 2010. \item PREDATOR : FP7 Collaborative Project on Design for predictability and efficiency. Feb 2008 -- Jan 2011. \item QUASIMODO : FP7 Collaborative Project on Quantitative system properties in model-driven design of embedded systems. Jan 2008 -- Dec 2010. \item MNEMEE : FP7 Collaborative Project on Memory management technology for adaptive and efficient design of embedded systems. Jan 2008--Dec 2010. \item INTERESTED: FP7 Collaborative Project on Interoperable embedded systems Tool-chain for enhanced rapid design, prototyping and code generation. Jan 2008--Dec 2010. \item PREDATOR : FP7 Collaborative Project on Design for predictability and efficiency. Feb 2008--Jan 2011. \item QUASIMODO : FP7 Collaborative Project on Quantitative system properties in model-driven design of embedded systems. Jan 2008--Dec 2010. \end{itemize} a large subset of C to some assembly language. It will already trace the evolution of selected high-level code fragments in order to relate them to low level code fragments and it will manifest cost annotations in the source low level code fragments, and it will manifest cost annotations in the source language.\\ \textbf{Target communities:} compiler developers; developers of code invariant analysis of assembly code.\\ Compiler developers will be interested by the techniques used to trace evolution Compiler developers will be interested in the techniques used to trace evolution of code fragments during compilation. They should also be interested in enhancing the proposed techniques to address more optimisations. suggesting enhancements to the proposed technique, in order to address more optimisations. Developers of code invariant generators will be able to apply and extend their Developers of tools for cache behaviour prediction and general analysis of assembly code should be particularly interested since our approach allows to reflect on the source code their own analysis performed on low level target reflect at the source code level their own analyses performed on low-level target code. \noindent \textbf{Dissemination:} Information dissemination on this activity will be done on the general project level, but will also try to target specific communities by targeted presentations/participation to relative conferences or meetings. \textbf{Dissemination:} Information dissemination for this activity will be done at the general project level, but will also try to target specific communities by targeted presentations/participation at relative conferences or meetings. In particular we plan to invite selected members of those communities to the first annual \cerco{} meeting to advertise the project results and foster annotations (produced by the compiler) and the complexity assertions (added by the user or synthesized automatically by abstract interpretation algorithms) in order to produce the right complexity obligations, that is the goal to be in order to produce the right complexity obligations, that is, the goal to be proved in order to check the correctness of the assertions.\\ \textbf{Target communities:} the interactive theorem proving community; Starting with the release of the prototype we will begin to contact potential end users, i.e. developers of time critical software, in order to attract feedback and to ensure that the final outcome fulfil actual requirements of the targeted exploitation community. feedback and to ensure that the final outcome will fulfil the specific requirements of the targeted exploitation community. \noindent \textbf{Dissemination:} Information dissemination on this activity will be done on the general project level, with particular attention to the interactive \textbf{Dissemination:} Information dissemination for this activity will be done at the general project level, with particular attention to the interactive theorem proving community. We will continue the practice of inviting selected members of the interested communities to the annual \cerco{} meetings to advertise the project results and foster annual \cerco{} meetings in order to advertise the project results and foster potential collaborations. Moreover we will gradually enlarge the scope of the dissemination activity from developers and researchers in formal methods to the wider audience of users of compilers that are potentially interested in exact execution time, even if at this stage we do not expect applications of the prototype to realistic programs. exact execution time, even if at this stage we do not expect the prototype compiler to apply to realistic programs. \subsection{Trusted CerCo compiler} \textbf{Description:} The trusted CerCo compiler is the final prototype of \cerco{} and it is composed of several components composed of several components: \begin{itemize} \item a proof of correctness in Matita of the and intensional behaviour of the program; \item an extension of the interactive theorem prover Matita with ad-hoc tactics and mechanism targeted towards the progressive automation --- either in the small or in the large --- of complexity theorem prover Matita with \emph{ad hoc} tactics and mechanisms targeted toward the progressive automation---either in the small or in the large---of complexity proofs; \item an extensive use case dedicated to the automatic generation of The interactive theorem proving community will benefit from the first fully open source proof of correctness of a realistic compiler for C written in the Calculus of (Co)Inductive Constructions and for a new technique to formally verify preservation of intentional properties without loosing precision. the Calculus of (Co)Inductive Constructions, and for a new technique for formally verifying preservation of intentional properties without losing precision. Developers of both interactive and automatic theorem provers will be interested in testing and enhancing their techniques when applied to automation of (or exact reaction time) for real time or synchronous programs and thus it is meant to attract interest from end users. In particular, we will be looking for feedback on the applicability of the proposed technique and we looking for feedback on the applicability of the proposed technique, and we will target in particular the sub-community of synchronous programmers. \noindent \textbf{Dissemination:} We will increase our dissemination activity during the last year of the project, in particular organizing separate events targeted to the scientific community and to the potential industrial stakeholders. We will final year of the project, in particular organizing separate events targeted at the scientific community and to potential industrial stakeholders. We will also improve accessibility and visibility of the \cerco{} compiler by developing packages for Linux distributions and Live CDs for non-Linux users. packages for Linux distributions, and Live CDs for non-Linux users. %\begin{thebibliography}{9}