Changeset 794 for Deliverables

May 12, 2011, 7:19:02 PM (10 years ago)
Ian Stark

Some content for addendum

1 edited


  • Deliverables/D6.2/addendum.tex

    r791 r794  
    99% 2011-05
    11 \documentclass[11pt,epsf,a4wide]{article}
    18 \vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
     20\vspace*{1cm}Project FP7-ICT-2009-C-243881 {\cerco}}
    2022\date{ }
    5557Main Authors:\\
    56 C. Sacerdoti Coen\\
    5758I. Stark
    63 Project Acronym: \cerco{}\\
     64Project Acronym: {\cerco}\\
    6465Project full title: Certified Complexity\\
    65 Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
    67 \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
     66Proposal/Contract no.: FP7-ICT-2009-C-243881 {\cerco}\\
     68\clearpage \pagestyle{myheadings} \markright{{\cerco}, FP7-ICT-2009-C-243881}
    72 Deliverable~6.2, the \emph{Plan for the Use and dissemination of foreground}
    73 was submitted as the first \textbf{report} of the \cerco{} project.  Following
    74 the scientific review of the project at the end of its first year, the
    75 reviewers recommended preparation of an addendum to specifically list future
     73Deliverable~6.2, the \emph{Plan for the Use and Dissemination of Foreground}
     74was submitted as the first report of the {\cerco} project.  Following the
     75scientific review of the project at the end of its first year, the reviewers
     76recommended preparation of an addendum to specifically list future
    7677dissemination plans.  This is that addendum.
    7980\section{Dissemination Plans}
    81 \subsection{Conferences}
     82The {\cerco} project represents an unprecedented effort to create a
     83machine-verified chain of trust for analysing program performance properties
     84through compilation.  This combines novel work in the theory of machine proof
     85and certified compilation with its concrete application to a specific
     86industrial microcontroller.
     88As appropriate for a project in the \emph{Future and Emerging Technologies}
     89programme, a major target for dissemination is to influence future work by
     90other European research groups, through a direct demonstration of a verified
     91resource-aware compiler.  The immediate routes for this are the standard ones
     92for academic communication and training: conference papers, journal articles,
     93collaborative workshops, tutorial events.  In addition, with the project
     94centred around a substantial implementation effort, the compiler code and the
     95machine proofs are themselves vehicles for dissemination to other researchers.
     97The longer-term dissemination targets are the potential end-users of verified
     98compiler technology: programmers of commodity microcontrollers being used in
     99tightly resource-constrained embedded applications --- particularly those
     100where safety-critical requirements mandate a high quality of performance
     101certification.  Possible routes for this long-term dissemination are through
     102research symposia at industrially-relevant conferences, and tutorial sessions
     103at conferences or other events with significant industrial presence.
     105\subsection{Conferences and Workshops}
     107We propose to submit results of {\cerco} research for presentation at
     108appropriate international venues.  There are very many conferences dealing
     109with {\cerco}-related areas: compilation technology, machine-assisted proof,
     110resource analysis, etc.  For example, the following are particularly close to
     111{\cerco} activity:
     113\item CPP: Certified Programs and Proofs
     114\item FMCAD: Formal Methods in Computer-Aided Design
     115\item LOLA: Syntax and Semantics of Low-Level Languages
     116\item VSTTE: Verified Software: Theories, Tools and Experiments
     117\item SSV: Systems Software Verification
     118\item FORMATS: Formal Modeling and Analysis of Timed Systems
     119\item ITP: Interactive Theorem Proving (was TPHOLs)
     120\item PSI: Program Understanding
     122Beyond these, there are many high-quality general conferences which would also
     123provide a good venue for publicising the results of the project.  For example:
     125\item POPL: Principles of Programming Languages
     126\item LPAR: Logic for Programming, Artificial Intelligence and Reasoning
     127\item CC: Compiler Construction
     128\item FM: International Symposium on Formal Methods
     129\item APLAS: Asian Symposium on Programming Languages and Reasoning
     131In addition to these subject-related events, {\cerco} will contribute to
     132FET-organized activities, such as conferences, dedicated workshops, working
     133groups and other meetings.
    85 \subsection{Workshops}
    87 \subsection{Tutorials}
     138The project participants will publish papers and articles based on {\cerco}
     139results in appropriate archival venues, throughout the duration of the
     140project.  Most of the conferences listed above have formal proceedings;
     141several also have affiliated special issues in journals, for publishing
     142extended versions of papers.  In addition, we expect to submit free-standing
     143articles to appropriate journals, such as:
     145\item Journal of Automated Reasoning
     146\item Journal of Formalized Reasoning
     147\item Information and Computation
     148\item Theoretical Computer Science
     149\item Higher-Order and Symbolic Computation
     150\item Communications of the ACM
     151\item Science of Computer Programming
     154\subsection{Tutorials and Training}
     156As established researchers, the project participants will give lectures and
     157tutorials on {\cerco}-related research as part of their existing dissemination
     158activity throughout the course of the project.  However, in addition to this
     159{\cerco} will organise specific training activities targeted at the scientific
     160community, and at potential industrial stakeholders.  These are formal
     161deliverables of Work Package~6 in the project contract.  To increase
     162visibility, and promote attendance, we would affiliate any event with an
     163existing conference or school.  For example, a {\cerco} tutorial would much
     164more effectively reach a suitable audience if given as part of an established
     165summer school.  It may also be appropriate to collaborate with related EU
     166projects or research groups in management of such events.
     168To benefit the most from {\cerco} project results, such events should take
     169place in the final year of the project.  We plan to identify appropriate
     170venues during the second year of {\cerco}.
     174A significant part of {\cerco} is the implementation effort, with accompanying
     175experience gained in developing and verifying a machine-checked resource-aware
     176compiler.  This gives rise to specific software artefacts, which other
     177projects can learn from and build upon.  All these will be made
     178publically-available at project milestones, and form a notable route for
     179dissemination of the project outcomes.  The full report D6.2 describes in
     180detail the target communities and potential users of this software; here we
     183\subsubsection{Untrusted Cost-Annotating Compiler}
     185This is a functional compiler from C to assembler, structured and instrumented
     186to trace the evolution of high-level code fragments to low-level instruction
     187sequences and match their execution costs.
     189\subsubsection{Untrusted Compiler within Proof-Assistant}
     191This will be an implementation of the CerCo cost-annotating compiler within
     192the \emph{Matita} proof assistant.  This takes the form of a formal
     193specification of the compiler in the calculus of (co)inductive constructions,
     194arranged in so as to be directly executable within \emph{Matita}. 
     196\subsubsection{Trusted Cost-Annotating Compiler}
     198This is the final product of the {\cerco} project and brings together a number
     199of distinct elements:
     201\item An executable compiler which automatically annotates C source code with
     202  machine execution costs;
     203\item A machine-certified proof that the compiler is functionally correct and
     204  that the automatic annotations exactly reflect low-level instruction costs;
     205\item Extensions to the \emph{Matita} interactive proof engine to automate
     206  this substantial proof;
     207\item Example integration of these low-level cost-annotations with high-level
     208  program analysis tools in the \emph{Frama-C} framework.
     214% LocalWords:  Sacerdoti Coen microcontroller FMCAD VSTTE TPHOLs LPAR Artefacts
Note: See TracChangeset for help on using the changeset viewer.