Changeset 48


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

finished touching up report's English

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D6.2/report.tex

    r47 r48  
    187187
    188188\subsection{Management of knowledge and intellectual property}
    189 All project partners have signed a Consortium Agreement before the start
    190 of the project, setting the principles of the consortium management and
    191 placing the relationship between the partners and their responsibilities on
    192 a legal basis for the duration of the work. In particular, the agreement
    193 includes specific arrangements concerning intellectual property rights to be
    194  applied among the participants and their affiliates, in compliance with the
    195 general arrangements stipulated in the contract.
    196 It thus specifies the rules
    197 for dissemination and use (confidentiality, ownership of results, patent rights,
    198 exploitation of results, protection and dissemination of knowledge), as well
    199 as financial and legal provisions.
    200 A peculiarity of \cerco{}
    201 is that we self-constrained to release open source software only, which is
    202 also manifest in our prototypes that will all be public, and that we did not
    203 identify any background to be protected.
     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.
    204202
    205203\subsection{Approach to Dissemination and Use}
    206204The \cerco{} project represents an unprecedented effort to create a verified
    207205chain of trust for intentional program properties during compilation,
    208 and we thus expect that it will generate in the short term a large interest in
    209 academia and in a longer term also a significant one in industry.
     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.
    210209
    211210Dissemination and use of foreground will have a high priority that will be
    212211intensified towards the end of the project and whose target will progressively
    213212shift from academia to potential end users.
    214 Work package 6 will be devoted to all the activities relevant to accomplishing this task.
    215 
    216     We have planned appropriate measures to ensure an effective and
    217 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
    218 long term kind, the main target of the dissemination activity will be research
    219 institutions that can immediately benefit from our results and that should take
    220 over the research effort after the end of \cerco{} to achieve the long terms
    221 results. We will also target industry by means of specific dissemination actions
    222 towards the end of the project in order to advertise our results and to ensure
    223 that the final outcome fulfil actual requirements of the industrial community.
     213Work package 6 will be devoted to all activities relevant to accomplishing this
     214task.
     215
     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.
    224226
    225227Dissemination will be carried out by a variety of means:
     
    230232 \item Publication of papers in proceedings of international conferences and
    231233       events, as well as in international scientific journals.
    232  \item Organization of meetings on project-related topics,
    233        including ``project workshops'' where attendance of external experts
     234 \item Organisation of meetings on project-related topics,
     235       including `project workshops' where attendance of external experts
    234236       and professionals is based on invitation.
    235  \item Organization of at least one special event targeted to the scientific
     237 \item Organisation of at least one special event targeted at the scientific
    236238       community, in the form of an open workshop, possibly affiliated to a
    237239       major conference, or in the form of courses given at summer schools
    238        or equivalent teaching events targeted to Ph.D. students.
    239  \item Organization of at least one special even targeted to potential
     240       or equivalent teaching events targeted to PhD students.
     241 \item Organisation of at least one special event targeted at potential
    240242       industrial stakeholders, in the form of a dissemination meeting to
    241243       be hold during the last year of the project.
    242  \item Design and management of a publicly available web-site that includes
     244 \item Design and management of a publicly available website that includes
    243245       descriptions of the main project results and allows the download of
    244246       all the software and publications developed in \cerco. The web-site will
     
    246248       users and researchers interested in the project.
    247249 \item Press conferences and press releases describing the advancement and
    248        main results of the project, so to reach and make the public aware of
     250       main results of the project, so as to reach and make the public aware of
    249251       both the short-term and long-term impact of the project results.
    250252 \item Dissemination of project objectives and results to members of
     
    257259The website of the \cerco{} project is
    258260\begin{center}\url{cerco.cs.unibo.it}\end{center}
    259 and it is made of a combination of a private and a public Wiki.
     261The website combines a private and public Wiki.
    260262The Wiki will progressively include:
    261263\begin{itemize}
    262264 \item A general introduction to the project: the objectives, the expected
    263265      results, the milestones, the detailed description of the consortium and
    264       its coordinates within the Seventh Framework Programme.
     266      its position within the Seventh Framework Programme.
    265267 \item The list of events taking place in the context of the project: meetings,
    266268      conferences, workshops, and their availability to the public.
    267  \item Publications originated from the project, both in the scientific community and in the general press.
     269 \item Publications originating with the project, both in the scientific
     270       community and in the general press.
    268271 \item A number of relevant links: other projects, institutions and companies
    269272      that are related to \cerco.
     
    276279       documents for the European Commission.
    277280 \item A private section containing contact details, mailing lists archives,
    278        details about the meetings (slides, notes and so on) and other
     281       details about meetings held (slides, notes and so on) and other
    279282       temporary technical information needed by the consortium.
    280283\end{itemize}
    281284
    282     Besides for the website, communication and information exchange among
    283 the members of the project is enforced via a carefully organized and maintained central repository and a number of dynamically created mailing lists.
    284 
    285 Ad-hoc advertisement of \cerco{} to the interested research communities will
     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.
     288
     289\emph{Ad hoc} advertisement of \cerco{} to the interested research communities will
    286290also be achieved by advertisements sent to the mailing lists of the projects,
    287291as well as advertisement of open job positions.
     
    289293\subsection{Project Workshops and Conferences, Lectures, Tutorials}
    290294Two Project Workshops will be organized every year.
    291 They will consist in a public and a private chapter and we will invite as
     295They will consist of a public and a private chapter and we will invite as
    292296guests a small number or international researchers who are working on related
    293297problems. We will try to co-locate later workshops with international events
    294 to improve visibility of the project. During the third year we plan as well to
    295 organize two separate additional events targeted to the scientific community
    296 and to potential industrial stakeholders.
     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.
    297301
    298302Moreover, we aim to present our work at international conferences and
     
    302306may be part of a more comprehensive presentation, it may get a presentation of
    303307its own, or even only special aspects of \cerco{} may be addressed by a talk.
    304 In the latter case some member of the group caring about the relative task
     308In the latter case some member of the group with expertise in the respective task
    305309or work-package may be the most suitable person to give the talk. Talks at
    306 larger conferences should be accompanied by papers on \cerco{} in the corresponding proceedings.
     310larger conferences should be accompanied by papers on \cerco{} in the
     311corresponding proceedings.
    307312
    308313\subsection{Publications}
    309314We aim to publish the results obtained in \cerco{} in the proceedings
    310315of international events and in international journals. The list of journals
    311 that publish papers related to the topics studied in \cerco{} comprises and
    312 it is not limited to the following ones:
     316that publish papers related to the topics studied in \cerco{} comprises, but
     317it is not limited to, the following ones:
    313318
    314319\begin{itemize}
     
    337342\subsection{Clustering}
    338343
    339 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.
     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.
    340347
    341348\subsubsection{National/Local Projects and Research Groups}
     
    345352
    346353\begin{itemize}
    347  \item CompCert \url{http://compcert.inria.fr}, the most advanced, closed
     354 \item CompCert \url{http://compcert.inria.fr}: the most advanced, closed
    348355       source project on the development of a certified compiler for a subset
    349        of C, and a natural source of inspiration and competitor for \cerco.
    350  \item Frama-C \url{http://frama-c.com}, an extensible and collaborative
     356       of C, and a natural source of inspiration (and competitor) for \cerco.
     357 \item Frama-C \url{http://frama-c.com}: an extensible and collaborative
    351358       platform dedicated to source-code analysis of C software. It is a
    352359       natural candidate for a technological integration with the \cerco{}
    353        compiler in order to provide high-level reasoning tools on the
     360       compiler, in order to provide high-level reasoning tools on the
    354361       intentional properties of C programs.
    355  \item AbsInt \url{http://absint.com} is a privately-held company located
    356        in Saarbruecken, Germany, that participated to several EU projects and
     362 \item AbsInt \url{http://absint.com}: a private company located
     363       in Saarbruecken, Germany, that participated in several EU projects and
    357364       has a good record of collaboration with the scientific community. It
    358365       develops advanced development tools for embedded systems, and tools for
     
    370377\item Embounded: FP6 Strep on Automatic Analysis of Bounded Resources for Embedded Systems.
    371378\item ARTISTDesign: FP7 Network of Excellence on Design of Embedded Systems
    372 \item MNEMEE : FP7 Collaborative Project on Memory management technology for adaptive and efficient design of embedded systems. Jan 2008 -- Dec 2010.
    373 \item INTERESTED: FP7 Collaborative Project on Interoperable embedded systems Tool-chain for enhanced rapid design, prototyping and code generation. Jan 2008 -- Dec 2010.
    374 \item PREDATOR : FP7 Collaborative Project on Design for predictability and efficiency. Feb 2008 -- Jan 2011.
    375 \item QUASIMODO : FP7 Collaborative Project on Quantitative system properties in model-driven design of embedded systems. Jan 2008 -- Dec 2010.
     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.
    376383\end{itemize}
    377384
     
    388395a large subset of C to some assembly language. It will already trace the
    389396evolution of selected high-level code fragments in order to relate them to
    390 low level code fragments and it will manifest cost annotations in the source
     397low level code fragments, and it will manifest cost annotations in the source
    391398language.\\
    392399\textbf{Target communities:} compiler developers; developers of code invariant
     
    394401analysis of assembly code.\\
    395402
    396 Compiler developers will be interested by the techniques used to trace evolution
     403Compiler developers will be interested in the techniques used to trace evolution
    397404of code fragments during compilation. They should also be interested in
    398 enhancing the proposed techniques to address more optimisations.
     405suggesting enhancements to the proposed technique, in order to address more
     406optimisations.
    399407
    400408Developers of code invariant generators will be able to apply and extend their
     
    404412Developers of tools for cache behaviour prediction and general analysis of
    405413assembly code should be particularly interested since our approach allows to
    406 reflect on the source code their own analysis performed on low level target
     414reflect at the source code level their own analyses performed on low-level target
    407415code.
    408416
    409417\noindent
    410 \textbf{Dissemination:} Information dissemination on this activity will be done
    411 on the general project level, but will also try to target specific communities
    412 by targeted presentations/participation to relative conferences or meetings.
     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.
    413421In particular we plan to invite selected members of those communities to the
    414422first annual \cerco{} meeting to advertise the project results and foster
     
    424432annotations (produced by the compiler) and the complexity assertions (added
    425433by the user or synthesized automatically by abstract interpretation algorithms)
    426 in order to produce the right complexity obligations, that is the goal to be
     434in order to produce the right complexity obligations, that is, the goal to be
    427435proved in order to check the correctness of the assertions.\\
    428436\textbf{Target communities:} the interactive theorem proving community;
     
    447455Starting with the release of the prototype we will begin to contact potential
    448456end users, i.e. developers of time critical software, in order to attract
    449 feedback and to ensure that the final outcome fulfil actual requirements of
    450 the targeted exploitation community.
     457feedback and to ensure that the final outcome will fulfil the specific
     458requirements of the targeted exploitation community.
    451459
    452460\noindent
    453 \textbf{Dissemination:} Information dissemination on this activity will be done
    454 on the general project level, with particular attention to the interactive
     461\textbf{Dissemination:} Information dissemination for this activity will be done
     462at the general project level, with particular attention to the interactive
    455463theorem proving community. We will continue the practice of inviting
    456464selected members of the interested communities to the
    457 annual \cerco{} meetings to advertise the project results and foster
     465annual \cerco{} meetings in order to advertise the project results and foster
    458466potential collaborations. Moreover we will gradually enlarge the scope of the
    459467dissemination activity from developers and researchers in formal methods to
    460468the wider audience of users of compilers that are potentially interested in
    461 exact execution time, even if at this stage we do not expect
    462 applications of the prototype to realistic programs.
     469exact execution time, even if at this stage we do not expect the prototype
     470compiler to apply to realistic programs.
    463471
    464472\subsection{Trusted CerCo compiler}
     
    466474\textbf{Description:}
    467475The trusted CerCo compiler is the final prototype of \cerco{} and it is
    468 composed of several components
     476composed of several components:
    469477\begin{itemize}
    470478 \item a proof of correctness in Matita of the
     
    472480and intensional behaviour of the program;
    473481 \item an extension of the interactive
    474 theorem prover Matita with ad-hoc tactics and mechanism targeted towards the
    475 progressive automation --- either in the small or in the large --- of complexity
     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
    476484proofs;
    477485 \item an extensive use case dedicated to the automatic generation of
     
    487495The interactive theorem proving community will benefit from the first fully
    488496open source proof of correctness of a realistic compiler for C written in
    489 the Calculus of (Co)Inductive Constructions and for a new technique to formally
    490 verify preservation of intentional properties without loosing precision.
     497the Calculus of (Co)Inductive Constructions, and for a new technique for formally
     498verifying preservation of intentional properties without losing precision.
    491499Developers of both interactive and automatic theorem provers will be interested
    492500in testing and enhancing their techniques when applied to automation of
     
    497505(or exact reaction time) for real time or synchronous programs and thus
    498506it is meant to attract interest from end users. In particular, we will be
    499 looking for feedback on the applicability of the proposed technique and we
     507looking for feedback on the applicability of the proposed technique, and we
    500508will target in particular the sub-community of synchronous programmers.
    501509
    502510\noindent
    503511\textbf{Dissemination:} We will increase our dissemination activity during the
    504 last year of the project, in particular organizing separate events targeted to
    505 the scientific community and to the potential industrial stakeholders. We will
     512final year of the project, in particular organizing separate events targeted at
     513the scientific community and to potential industrial stakeholders. We will
    506514also improve accessibility and visibility of the \cerco{} compiler by developing
    507 packages for Linux distributions and Live CDs for non-Linux users.
     515packages for Linux distributions, and Live CDs for non-Linux users.
    508516
    509517%\begin{thebibliography}{9}
Note: See TracChangeset for help on using the changeset viewer.