1 | \documentclass[11pt,epsf,a4wide]{article} |
---|
2 | \usepackage{../style/cerco} |
---|
3 | |
---|
4 | \title{ |
---|
5 | INFORMATION AND COMMUNICATION TECHNOLOGIES\\ |
---|
6 | (ICT)\\ |
---|
7 | PROGRAMME\\ |
---|
8 | \vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}} |
---|
9 | |
---|
10 | \date{ } |
---|
11 | \author{} |
---|
12 | |
---|
13 | \begin{document} |
---|
14 | \thispagestyle{empty} |
---|
15 | |
---|
16 | \vspace*{-1cm} |
---|
17 | \begin{center} |
---|
18 | \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png} |
---|
19 | \end{center} |
---|
20 | |
---|
21 | \begin{minipage}{\textwidth} |
---|
22 | \maketitle |
---|
23 | \end{minipage} |
---|
24 | |
---|
25 | |
---|
26 | \vspace*{0.5cm} |
---|
27 | \begin{center} |
---|
28 | \begin{LARGE} |
---|
29 | \bf |
---|
30 | Report n. D6.2\\ |
---|
31 | Plan for the Use and dissemination of foreground\\ |
---|
32 | \end{LARGE} |
---|
33 | \end{center} |
---|
34 | |
---|
35 | \vspace*{2cm} |
---|
36 | \begin{center} |
---|
37 | \begin{large} |
---|
38 | Version 1.0 |
---|
39 | \end{large} |
---|
40 | \end{center} |
---|
41 | |
---|
42 | \vspace*{0.5cm} |
---|
43 | \begin{center} |
---|
44 | \begin{large} |
---|
45 | Main Authors:\\ |
---|
46 | C. Sacerdoti Coen |
---|
47 | \end{large} |
---|
48 | \end{center} |
---|
49 | |
---|
50 | \vspace*{\fill} |
---|
51 | \noindent |
---|
52 | Project Acronym: \cerco{}\\ |
---|
53 | Project full title: Certified Complexity\\ |
---|
54 | Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\ |
---|
55 | |
---|
56 | \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881} |
---|
57 | |
---|
58 | \tableofcontents |
---|
59 | |
---|
60 | \section{Premise} |
---|
61 | The deliverable D6.2 \emph{Plan for the Use and dissemination of foreground} |
---|
62 | is the first \textbf{report} of the \cerco{} project. The deliverable is |
---|
63 | \textbf{confidential} and required an effort of about \textbf{2 person-months}. |
---|
64 | The description of the deliverable in the Grant Agreement is the following one: |
---|
65 | \begin{quote} |
---|
66 | Plan for the Use and dissemination of foreground: An articulated dissemination plan, containing the individuation of the main target communities, and the relative exploitation strategies. |
---|
67 | \end{quote} |
---|
68 | |
---|
69 | %{\textbf |
---|
70 | %COMMISSION REQUIREMENTS: |
---|
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. |
---|
72 | % |
---|
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. |
---|
74 | % |
---|
75 | %3. Exploitable results |
---|
76 | % |
---|
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. |
---|
78 | % |
---|
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: |
---|
80 | % |
---|
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); |
---|
82 | % |
---|
83 | % * Customer detection: identification of the potential customers and the factors that affect their purchasing decisions; |
---|
84 | % |
---|
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; |
---|
86 | % |
---|
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. |
---|
88 | % |
---|
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. |
---|
90 | %} |
---|
91 | |
---|
92 | \section{Overview and General Approach} |
---|
93 | \subsection{Overview of expected results} |
---|
94 | Driven by a growing confidence in formal methods in general and interactive |
---|
95 | theorem proving in particular, critical IT systems are slowly undergoing a |
---|
96 | paradigm shift: testing of critical properties is going to be partially |
---|
97 | replaced with formal verification on the programs written in an high level |
---|
98 | language, and a set of formally verified tools (interpreters, compilers, |
---|
99 | operating systems, communication libraries) is going to be used to grant preservation |
---|
100 | of the verified property for the actual runs of the low level code. |
---|
101 | |
---|
102 | The present state of the art already provides a few mildly optimizing |
---|
103 | verified compilers that compete with traditional highly optimized compilers |
---|
104 | and a few prototypes and experiments in the verification of operating systems. |
---|
105 | However, the only properties that have been formalized are extensional, granting |
---|
106 | that the high level semantics of the program --- usually specified in terms |
---|
107 | of infinite resources (e.g. memory) --- is respected. All intensional |
---|
108 | properties that have to do with resources are not currently preserved during |
---|
109 | compilation or, at least, no formal proof of preservation is provided. Hence |
---|
110 | high level programs still need to be extensively tested to verify resource |
---|
111 | related properties like memory consumption or reaction time for reactive |
---|
112 | and real time programs. |
---|
113 | |
---|
114 | In \cerco{} we will address intentional properties of programs, in particular |
---|
115 | execution time, and we will develop the first certified compiler that is able |
---|
116 | to manifest in the source program some intentional properties, mainly |
---|
117 | execution cost, that are inferred from the target program. The main issue |
---|
118 | in doing so is to preserve compositionality of compilation: while the source |
---|
119 | program undergoes several intentionally disruptive translations towards lower |
---|
120 | and lower intermediate languages, we need to keep trace of the evolution of |
---|
121 | sensible code fragments in order to relate source, intermediate and target |
---|
122 | code fragments to back-propagate execution costs. Hence we expect to study |
---|
123 | new more refined ways of expressing the operational semantics of programs |
---|
124 | and to give a more refined notion of operational bisimulation, with the aim |
---|
125 | of obtaining a characterization that is loose enough to capture some of the |
---|
126 | most common and effective optimizations. |
---|
127 | |
---|
128 | Once we can manifest in the source program execution costs computed on the |
---|
129 | target program we will start the investigation of the exploitability of the |
---|
130 | cost annotations. In particular, cost annotations must be combined with |
---|
131 | extensional program invariants in order to obtain intensional program invariants |
---|
132 | and be able to formally prove intensional properties of programs. We expect |
---|
133 | this study to require a long effort and to be performed outside the project |
---|
134 | timeframe. However, we assume that a combination of interactive theorem proving |
---|
135 | and automatic formal methods (like abstract interpretation) will need to be |
---|
136 | exploited and, in the project, we will focus on interactive theorem proving by |
---|
137 | exploiting and providing basic tools to reason on cost invariants. |
---|
138 | |
---|
139 | All the major deliverables of \cerco{} are prototypes --- either software |
---|
140 | prototypes or formal certifications --- that are later integrated at project |
---|
141 | milestones into major \cerco{} compiler snapshots. These snapshots are the |
---|
142 | most appropriate deliverables for dissemination in the large and different |
---|
143 | target communities are associated to the snapshots. We will discuss |
---|
144 | the milestones and snapshots in details |
---|
145 | in Section~\ref{byresult} in order to identify the potential target communities |
---|
146 | and relative specific dissemination actions. |
---|
147 | |
---|
148 | |
---|
149 | ~\\ |
---|
150 | |
---|
151 | \begin{center} |
---|
152 | \begin{tabular}{|lc|} |
---|
153 | \hline |
---|
154 | milestone name & due at month \\ \hline |
---|
155 | Untrusted cost-annotating compiler & 12 \\ |
---|
156 | Untrusted CerCo compiler & 24 \\ |
---|
157 | Trusted CerCo compiler & 36 \\ |
---|
158 | \hline |
---|
159 | \end{tabular} |
---|
160 | \end{center} |
---|
161 | |
---|
162 | ~\\ |
---|
163 | |
---|
164 | \subsection{Academic exploitation} |
---|
165 | Academic partners will take great advantage from the results of CerCo mainly in terms of increased technical know-how and scientific knowledge, increased visibility in the scientific community of reference, increased expertise, exploitable for institutional academic purposes (e.g. didactic activities). We also expect that the rest of the academic community will take up the innovative ideas of the project, building on top of them code analyses at a level of accuracy that could have not been previously possible. Finally, we expect elaboration and instantiation of our methodology to other kinds of high level languages (functional, logic) and to more complex scenarios involving, for instance, a real time operating system. |
---|
166 | |
---|
167 | \subsection{Industrial exploitation} |
---|
168 | The long term industrial exploitation of the results of the CerCo project is envisaged mainly in the area of the embedded systems/software, in particular in the case of safety critical applications and time critical (realtime) applications. In the short term, software houses producing compilers for embedded systems could immediately benefit from the CerCo cost annotating technology or, more generally, by the know- how provided in the certification of compilers. It is worth noting that several of these software houses are located in Europe, such as the medium-sized System Engineer Group of Freescale, which is headquartered in Scotland, Raisonance and Cosmic Software, which are headquartered in France, the small-size Hightech, headquartered in Germany, just to name a few. |
---|
169 | |
---|
170 | \subsection{Management of knowledge and intellectual property} |
---|
171 | All project partners have signed a Consortium Agreement before the start |
---|
172 | of the project, setting the principles of the consortium management and |
---|
173 | placing the relationship between the partners and their responsibilities on |
---|
174 | a legal basis for the duration of the work. In particular, the agreement |
---|
175 | includes specific arrangements concerning intellectual property rights to be |
---|
176 | applied among the participants and their affiliates, in compliance with the |
---|
177 | general arrangements stipulated in the contract. |
---|
178 | It thus specifies the rules |
---|
179 | for dissemination and use (confidentiality, ownership of results, patent rights, |
---|
180 | exploitation of results, protection and dissemination of knowledge), as well |
---|
181 | as financial and legal provisions. |
---|
182 | A peculiarity of \cerco{} |
---|
183 | is that we self-constrained to release open source software only, which is |
---|
184 | also manifest in our prototypes that will all be public, and that we did not |
---|
185 | identify any background to be protected. |
---|
186 | |
---|
187 | \subsection{Approach to Dissemination and Use} |
---|
188 | The \cerco{} project represents an unprecedented effort to create a verified |
---|
189 | chain of trust for intentional program properties during compilation, |
---|
190 | and we thus expect that it will generate in the short term a large interest in |
---|
191 | academia and in a longer term also a significant one in industry. |
---|
192 | |
---|
193 | Dissemination and use of foreground will have a high priority that will be |
---|
194 | intensified towards the end of the project and whose target will progressively |
---|
195 | shift from academia to potential end users. |
---|
196 | Work package 6 will be devoted to all the activities relevant to accomplishing this task. |
---|
197 | |
---|
198 | We have planned appropriate measures to ensure an effective and |
---|
199 | 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 |
---|
200 | long term kind, the main target of the dissemination activity will be research |
---|
201 | institutions that can immediately benefit from our results and that should take |
---|
202 | over the research effort after the end of \cerco{} to achieve the long terms |
---|
203 | results. We will also target industry by means of specific dissemination actions |
---|
204 | towards the end of the project in order to advertise our results and to ensure |
---|
205 | that the final outcome fulfil actual requirements of the industrial community. |
---|
206 | |
---|
207 | Dissemination will be carried out by a variety of means: |
---|
208 | \begin{itemize} |
---|
209 | \item Talks at relevant international conferences, events and forums (both |
---|
210 | presenting the technical achievements and introducing at a high level |
---|
211 | the project’s objectives and results). |
---|
212 | \item Publication of papers in proceedings of international conferences and |
---|
213 | events, as well as in international scientific journals. |
---|
214 | \item Organization of meetings on project-related topics, |
---|
215 | including ``project workshops'' where attendance of external experts |
---|
216 | and professionals is based on invitation. |
---|
217 | \item Organization of at least one special event targeted to the scientific |
---|
218 | community, in the form of an open workshop, possibly affiliated to a |
---|
219 | major conference, or in the form of courses given at summer schools |
---|
220 | or equivalent teaching events targeted to Ph.D. students. |
---|
221 | \item Organization of at least one special even targeted to potential |
---|
222 | industrial stakeholders, in the form of a dissemination meeting to |
---|
223 | be hold during the last year of the project. |
---|
224 | \item Design and management of a publicly available web-site that includes |
---|
225 | descriptions of the main project results and allows the download of |
---|
226 | all the software and publications developed in \cerco. The web-site will |
---|
227 | be managed as a Wiki to maximise interaction with the community of |
---|
228 | users and researchers interested in the project. |
---|
229 | \item Press conferences and press releases describing the advancement and |
---|
230 | main results of the project, so to reach and make the public aware of |
---|
231 | both the short-term and long-term impact of the project results. |
---|
232 | \item Dissemination of project objectives and results to members of |
---|
233 | European or national level projects having \cerco{} members as |
---|
234 | participants. |
---|
235 | \end{itemize} |
---|
236 | |
---|
237 | \section{Description of the Dissemination Plan} |
---|
238 | \subsection{Web presence and information exchange} |
---|
239 | The website of the \cerco{} project is |
---|
240 | \begin{center}\url{cerco.cs.unibo.it}\end{center} |
---|
241 | and it is made of a combination of a private and a public Wiki. |
---|
242 | The Wiki will progressively include: |
---|
243 | \begin{itemize} |
---|
244 | \item A general introduction to the project: the objectives, the expected |
---|
245 | results, the milestones, the detailed description of the consortium and |
---|
246 | its coordinates within the Seventh Framework Programme. |
---|
247 | \item The list of events taking place in the context of the project: meetings, |
---|
248 | conferences, workshops, and their availability to the public. |
---|
249 | \item Publications originated from the project, both in the scientific community and in the general press. |
---|
250 | \item A number of relevant links: other projects, institutions and companies |
---|
251 | that are related to \cerco. |
---|
252 | \item A public section containing the public deliverables, comprising the |
---|
253 | open source software developed in \cerco. In order to make a first |
---|
254 | trial of the software as simple as possible for interested users, |
---|
255 | we plan to provide packages for some common Linux distributions and |
---|
256 | a Live CD for non Linux users. |
---|
257 | \item A private section containing the remaining deliverables and other |
---|
258 | documents for the European Commission. |
---|
259 | \item A private section containing contact details, mailing lists archives, |
---|
260 | details about the meetings (slides, notes and so on) and other |
---|
261 | temporary technical information needed by the consortium. |
---|
262 | \end{itemize} |
---|
263 | |
---|
264 | Besides for the website, communication and information exchange among |
---|
265 | the members of the project is enforced via a carefully organized and maintained central repository and a number of dynamically created mailing lists. |
---|
266 | |
---|
267 | Ad-hoc advertisement of \cerco{} to the interested research communities will |
---|
268 | also be achieved by advertisements sent to the mailing lists of the projects, |
---|
269 | as well as advertisement of open job positions. |
---|
270 | |
---|
271 | \subsection{Project Workshops and Conferences, Lectures, Tutorials} |
---|
272 | Two Project Workshops will be organized every year. |
---|
273 | They will consist in a public and a private chapter and we will invite as |
---|
274 | guests a small number or international researchers who are working on related |
---|
275 | problems. We will try to co-locate later workshops with international events |
---|
276 | to improve visibility of the project. During the third year we plan as well to |
---|
277 | organize two separate additional events targeted to the scientific community |
---|
278 | and to potential industrial stakeholders. |
---|
279 | |
---|
280 | Moreover, we aim to present our work at international conferences and |
---|
281 | forums on interactive and automatic theorem proving, resource aware computing, |
---|
282 | invariant generation, formal methods and reactive computing. In accordance |
---|
283 | with the character of the corresponding meeting, the presentation of \cerco{} |
---|
284 | may be part of a more comprehensive presentation, it may get a presentation of |
---|
285 | its own, or even only special aspects of \cerco{} may be addressed by a talk. |
---|
286 | In the latter case some member of the group caring about the relative task |
---|
287 | or work-package may be the most suitable person to give the talk. Talks at |
---|
288 | larger conferences should be accompanied by papers on \cerco{} in the corresponding proceedings. |
---|
289 | |
---|
290 | \subsection{Publications} |
---|
291 | We aim to publish the results obtained in \cerco{} in the proceedings |
---|
292 | of international events and in international journals. The list of journals |
---|
293 | that publish papers related to the topics studied in \cerco{} comprises and |
---|
294 | it is not limited to the following ones: |
---|
295 | |
---|
296 | \begin{itemize} |
---|
297 | \item Journal of Automated Reasoning |
---|
298 | \item Journal of Formalized Reasoning |
---|
299 | \item Information and Computation |
---|
300 | \item Higher-Order and Symbolic Computation |
---|
301 | \item Communications of the ACM |
---|
302 | \item Science of computer programming |
---|
303 | \end{itemize} |
---|
304 | |
---|
305 | Many international conferences and workshops deal with compilation, |
---|
306 | formal reasonings and resource analysis. Some of the most important are |
---|
307 | certainly |
---|
308 | |
---|
309 | \begin{itemize} |
---|
310 | \item Principles of Programming Languages (POPL) |
---|
311 | \item Interactive Theorem Proving (ITP, ex TPHOLs) |
---|
312 | \item Logic for Programming, Artificial Intelligence and Reasoning (LPAR) |
---|
313 | \item Compiler Construction (CC) |
---|
314 | \item International Symposium on Formal Methods (FM) |
---|
315 | \item Symposium on Programming Languages and Reasoning (APLAS) |
---|
316 | %\item Types for Proofs and Programs (TYPEs) |
---|
317 | \end{itemize} |
---|
318 | |
---|
319 | \subsection{Clustering} |
---|
320 | |
---|
321 | 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. |
---|
322 | |
---|
323 | \subsubsection{National/Local Projects and Research Groups} |
---|
324 | |
---|
325 | The following national/local projects and research groups are the most direct |
---|
326 | interlocutors for \cerco. |
---|
327 | |
---|
328 | \begin{itemize} |
---|
329 | \item CompCert \url{http://compcert.inria.fr}, the most advanced, closed |
---|
330 | source project on the development of a certified compiler for a subset |
---|
331 | of C, and a natural source of inspiration and competitor for \cerco. |
---|
332 | \item Frama-C \url{http://frama-c.com}, an extensible and collaborative |
---|
333 | platform dedicated to source-code analysis of C software. It is a |
---|
334 | natural candidate for a technological integration with the \cerco{} |
---|
335 | compiler in order to provide high-level reasoning tools on the |
---|
336 | intentional properties of C programs. |
---|
337 | \item AbsInt \url{http://absint.com} is a privately-held company located |
---|
338 | in Saarbruecken, Germany, that participated to several EU projects and |
---|
339 | has a good record of collaboration with the scientific community. It |
---|
340 | develops advanced development tools for embedded systems, and tools for |
---|
341 | validation, verification and certification of safety-critical software. |
---|
342 | \end{itemize} |
---|
343 | |
---|
344 | \subsubsection{EU Projects} |
---|
345 | |
---|
346 | This is a selection of EU projects (mainly from FP7) dealing with embedded or, |
---|
347 | more generally, resource constrained systems. |
---|
348 | |
---|
349 | \begin{itemize} |
---|
350 | \item ARTEMIS: European Technology Platform/Joint Technology Initiative on |
---|
351 | Advanced Research \& Technology for Embedded Intelligence and Systems |
---|
352 | \item Embounded: FP6 Strep on Automatic Analysis of Bounded Resources for Embedded Systems. |
---|
353 | \item ARTISTDesign: FP7 Network of Excellence on Design of Embedded Systems |
---|
354 | \item MNEMEE : FP7 Collaborative Project on Memory management technology for adaptive and efficient design of embedded systems. Jan 2008 -- Dec 2010. |
---|
355 | \item INTERESTED: FP7 Collaborative Project on Interoperable embedded systems Tool-chain for enhanced rapid design, prototyping and code generation. Jan 2008 -- Dec 2010. |
---|
356 | \item PREDATOR : FP7 Collaborative Project on Design for predictability and efficiency. Feb 2008 -- Jan 2011. |
---|
357 | \item QUASIMODO : FP7 Collaborative Project on Quantitative system properties in model-driven design of embedded systems. Jan 2008 -- Dec 2010. |
---|
358 | \end{itemize} |
---|
359 | |
---|
360 | \section{Description of the Use Plan (by result)}\label{byresult} |
---|
361 | |
---|
362 | In this section, we describe the expected project results that are released |
---|
363 | in correspondence with project milestones and that have potential |
---|
364 | for exploitation. |
---|
365 | |
---|
366 | \subsection{Untrusted cost-annotating compiler} |
---|
367 | \textbf{Delivery date:} January 2011\\ |
---|
368 | \textbf{Description:} |
---|
369 | The untrusted cost-annotating compiler will be a functional compiler from |
---|
370 | a large subset of C to some assembly language. It will already trace the |
---|
371 | evolution of selected high-level code fragments in order to relate them to |
---|
372 | low level code fragments and it will manifest cost annotations in the source |
---|
373 | language.\\ |
---|
374 | \textbf{Target communities:} compiler developers; developers of code invariant |
---|
375 | generators; developers of tools for cache behaviour prediction and general |
---|
376 | analysis of assembly code.\\ |
---|
377 | |
---|
378 | Compiler developers will be interested by the techniques used to trace evolution |
---|
379 | of code fragments during compilation. They should also be interested in |
---|
380 | enhancing the proposed techniques to address more optimizations. |
---|
381 | |
---|
382 | Developers of code invariant generators will be able to apply and extend their |
---|
383 | own techniques to deal with exact execution time by considering cost annotations |
---|
384 | during the invariant generation phase. |
---|
385 | |
---|
386 | Developers of tools for cache behaviour prediction and general analysis of |
---|
387 | assembly code should be particularly interested since our approach allows to |
---|
388 | reflect on the source code their own analysis performed on low level target |
---|
389 | code. |
---|
390 | |
---|
391 | \noindent |
---|
392 | \textbf{Dissemination:} Information dissemination on this activity will be done |
---|
393 | on the general project level, but will also try to target specific communities |
---|
394 | by targeted presentations/participation to relative conferences or meetings. |
---|
395 | In particular we plan to invite selected members of those communities to the |
---|
396 | first annual \cerco{} meeting to advertise the project results and foster |
---|
397 | potential collaborations. |
---|
398 | |
---|
399 | \subsection{Untrusted CerCo compiler} |
---|
400 | \textbf{Delivery date:} January 2012\\ |
---|
401 | \textbf{Description:} |
---|
402 | The CerCo compiler will be a re-implementation of the untrusted cost-annotating |
---|
403 | compiler in the variant of the Calculus of (Co)Inductive Constructions |
---|
404 | implemented by Matita, ready to be certified. Moreover, it will enhance the |
---|
405 | previous prototype by integrating a new layer for the management of cost |
---|
406 | annotations (produced by the compiler) and the complexity assertions (added |
---|
407 | by the user or synthesized automatically by abstract interpretation algorithms) |
---|
408 | in order to produce the right complexity obligations, that is the goal to be |
---|
409 | proved in order to check the correctness of the assertions.\\ |
---|
410 | \textbf{Target communities:} the interactive theorem proving community; |
---|
411 | developers of code invariant generators; the abstract interpretation |
---|
412 | community; end users.\\ |
---|
413 | |
---|
414 | The interactive theorem proving community will benefit from an executable |
---|
415 | specification of a realistic compiler for C written in |
---|
416 | the Calculus of (Co)Inductive Constructions. However, at this stage the |
---|
417 | main benefit for the community will be a project by-product, which is |
---|
418 | a low level executable semantics (an interpreter) for some |
---|
419 | target machine and for several intermediate languages, that could easily be |
---|
420 | reused in other formalizations and translated to other interactive theorem |
---|
421 | provers. |
---|
422 | |
---|
423 | Developers of code invariant generators and the abstract interpretation |
---|
424 | community should be interested in the new layer of management of cost |
---|
425 | annotations and complexity assertions in order to interface their techniques on |
---|
426 | top of it or to propose alternative management approaches. The prototype could |
---|
427 | also be used as a test-bench generator for their techniques. |
---|
428 | |
---|
429 | Starting with the release of the prototype we will begin to contact potential |
---|
430 | end users, i.e. developers of time critical software, in order to attract |
---|
431 | feedback and to ensure that the final outcome fulfil actual requirements of |
---|
432 | the targeted exploitation community. |
---|
433 | |
---|
434 | \noindent |
---|
435 | \textbf{Dissemination:} Information dissemination on this activity will be done |
---|
436 | on the general project level, with particular attention to the interactive |
---|
437 | theorem proving community. We will continue the practice of inviting |
---|
438 | selected members of the interested communities to the |
---|
439 | annual \cerco{} meetings to advertise the project results and foster |
---|
440 | potential collaborations. Moreover we will gradually enlarge the scope of the |
---|
441 | dissemination activity from developers and researchers in formal methods to |
---|
442 | the wider audience of users of compilers that are potentially interested in |
---|
443 | exact execution time, even if at this stage we do not expect |
---|
444 | applications of the prototype to realistic programs. |
---|
445 | |
---|
446 | \subsection{Trusted CerCo compiler} |
---|
447 | \textbf{Delivery date:} January 2013\\ |
---|
448 | \textbf{Description:} |
---|
449 | The trusted CerCo compiler is the final prototype of \cerco{} and it is |
---|
450 | composed of several components |
---|
451 | \begin{itemize} |
---|
452 | \item a proof of correctness in Matita of the |
---|
453 | compliance of the compiler, described as preservation of both the extensional |
---|
454 | and intensional behaviour of the program; |
---|
455 | \item an extension of the interactive |
---|
456 | theorem prover Matita with ad-hoc tactics and mechanism targeted towards the |
---|
457 | progressive automation --- either in the small or in the large --- of complexity |
---|
458 | proofs; |
---|
459 | \item an extensive use case dedicated to the automatic generation of |
---|
460 | cost invariants for the C code generated by a synchronous language compiler. |
---|
461 | The functionalities developed in the use case will be tested to compute |
---|
462 | certified reaction time bounds for significant examples of synchronous |
---|
463 | programs. |
---|
464 | \end{itemize} |
---|
465 | \textbf{Target communities:} the interactive and automatic theorem proving |
---|
466 | community; developers of code invariant generators; end users, in particular |
---|
467 | synchronous languages programmers.\\ |
---|
468 | |
---|
469 | The interactive theorem proving community will benefit from the first fully |
---|
470 | open source proof of correctness of a realistic compiler for C written in |
---|
471 | the Calculus of (Co)Inductive Constructions and for a new technique to formally |
---|
472 | verify preservation of intentional properties without loosing precision. |
---|
473 | Developers of both interactive and automatic theorem provers will be interested |
---|
474 | in testing and enhancing their techniques when applied to automation of |
---|
475 | complexity proofs. |
---|
476 | |
---|
477 | The final prototype of the \cerco{} project is supposed to be the first |
---|
478 | realistic milestone towards the formal certification of exact execution time |
---|
479 | (or exact reaction time) for real time or synchronous programs and thus |
---|
480 | it is meant to attract interest from end users. In particular, we will be |
---|
481 | looking for feedback on the applicability of the proposed technique and we |
---|
482 | will target in particular the sub-community of synchronous programmers. |
---|
483 | |
---|
484 | \noindent |
---|
485 | \textbf{Dissemination:} We will increase our dissemination activity during the |
---|
486 | last year of the project, in particular organizing separate events targeted to |
---|
487 | the scientific community and to the potential industrial stakeholders. We will |
---|
488 | also improve accessibility and visibility of the \cerco{} compiler by developing |
---|
489 | packages for Linux distributions and Live CDs for non-Linux users. |
---|
490 | |
---|
491 | %\begin{thebibliography}{9} |
---|
492 | %\bibitem{matita} The Interactive Theorem Prover Matita, |
---|
493 | % \url{http://matita.cs.unibo.it} |
---|
494 | %\bibitem{subversion}The Version Control System Subversion, |
---|
495 | % \url{http://subversion.apache.org} |
---|
496 | %\bibitem{trac}The Integrated SCM \& Project Management tool Trac, |
---|
497 | % \url{http://trac.edgewall.org} |
---|
498 | %\end{thebibliography} |
---|
499 | |
---|
500 | \end{document} |
---|