source: Deliverables/D1.1/Presentations/WP1-claudio.tex @ 672

Last change on this file since 672 was 665, checked in by sacerdot, 9 years ago

...

File size: 23.5 KB
Line 
1\documentclass{beamer}
2
3\usetheme{Frankfurt}
4\logo{\includegraphics[height=1.0cm]{fetopen.png}}
5
6\usepackage{amsfonts}
7\usepackage{amsmath}
8\usepackage{eurosym}
9\usepackage{amssymb}
10\usepackage[english]{babel}
11\usepackage{color}
12\usepackage[utf8x]{inputenc}
13\usepackage{listings}
14\usepackage{stmaryrd}
15\usepackage{fancyvrb}
16% \usepackage{microtype}
17
18\author{Claudio Sacerdoti Coen}
19\title{Certified Complexity (CerCo)\\
20       Overall Presentation and Project Managemnt}
21\date{March 11, 2011}
22
23\setlength{\parskip}{1em}
24
25\AtBeginSection[]
26{
27  \begin{frame}<beamer>
28    \frametitle{Outline}
29    \tableofcontents[currentsection]
30  \end{frame}
31}
32
33\begin{document}
34
35\begin{frame}
36\maketitle
37\end{frame}
38
39\begin{frame}
40  \frametitle{Outline}
41  \tableofcontents
42\end{frame}
43
44\section{Long, middle and short term objectives}
45
46\begin{frame}
47 \frametitle{The ICT of the future}
48 We envision a (long term) future where formal methods will be pervasive:
49 \begin{center}
50   \alert{\Large Most programs will be (partially) specified and certified}
51 \end{center}
52
53 The very same definition of ``program'' will change:
54 \begin{center}
55  \alert{\Large A program will be a triple made of a specification,
56  an implementation and a proof certificate}
57 \end{center}
58
59 Cfr: Proof Carrying Code (PCC)
60\end{frame}
61
62\begin{frame}
63 \frametitle{The ICT of the future}
64 Signals in this direction:
65
66 \begin{itemize}
67  \item Formal methods are more and more embraced in industry
68  \item If total certification remains mostly unfeasible,
69        techniques for pay-as-you-ride certification are reaching larger
70        audiences\\
71        (model checking, type systems, abstract interpretation, dependent
72         types, \ldots)
73  \item Larger varities of user-friendly tools for partial certifications\\
74        (termination checkers, WCET analyzers, source code analyzers based
75         on WP, \ldots)
76  \item New open tools that integrate collaborating plug-ins to perform
77        automatic or interactive analyses (e.g. Frama-C)
78 \end{itemize}
79\end{frame}
80
81\begin{frame}
82 \frametitle{The ICT of the future}
83 Compiler = a tool to translates programs
84  \alert{preserving something}\\~\\
85
86 In our long-term vision:
87 \begin{center}
88 \alert{\Large A compiler maps triples specification-implementation-certificate
89  to triples specification-implementation-certificate.}
90 \end{center}
91
92 Questions:
93 \begin{enumerate}
94  \item What properties are \alert{preserved} during compilation?
95  \item What properties are \alert{affected} by the compilation strategy?
96  \item To what extent can you trust your compiler in preserving those properties?
97 \end{enumerate}
98\end{frame}
99
100\begin{frame}
101 \frametitle{The ICT of the future}
102 Preservation of properties during compilation:
103 \begin{itemize}
104  \item Extensional properties are easily specifiable and easily preserved
105        during compilation, but \alert{only assuming infinite resources}
106  \item Little is known even foundationally on the
107        \alert{preservation of intensional properties}
108        (e.g. use of space, time, energy)
109  \item For sure \alert{compilation} (which is not compositional)
110        \alert{affects the intensional properties}\\
111        E.g. the cost of different occurrences of $x+1$ can be different
112  \item Hence \alert{how} can you \alert{specify} intensional properties
113        as a function of the compilation strategy?
114 \end{itemize}
115\end{frame}
116
117\begin{frame}
118 \frametitle{Long term theoretical objectives}
119 \begin{enumerate}
120  \item to study the \alert{specification} of intensional properties
121        under \alert{realistic and precise cost models} induced by the
122        compilation strategy
123  \item to study \alert{preservation} of extensional and intensional
124        properties (\alert{under finiteness assumption})
125 \end{enumerate}
126
127 Byproducts:
128 \begin{enumerate}
129  \item being able to prove the efficacity of optimizations
130  \item being able to state completeness of compilation under
131        finiteness assumptions
132 \end{enumerate}
133\end{frame}
134
135\begin{frame}
136 \frametitle{Long term practical objectives}
137 \begin{enumerate}
138  \item allow developers of \alert{(hard) real time systems} to comfortably
139    prove meeting of deadline on \alert{high level languages} with the guarantee
140    that they hold on the object code
141  \item allow developers of \alert{embedded systems} to reason on
142    \alert{resource consumption} on \alert{high level languages} with the same
143     guarantee
144  \item augment the \alert{precision of formal methods} for intensional
145    properties on high level languages
146  \item obtain a new generation of \alert{precise and fully trustable WCET}
147    analyzers
148 \end{enumerate}
149\end{frame}
150
151\begin{frame}
152 \frametitle{Short term objectives}
153 \begin{enumerate}
154  \item develop a \alert{compiler} from
155        \alert{$\approx\!\!$ C} to the \alert{MCS-51} microprocessor
156        used for embedded systems
157  \item have the compiler infer from the assembly code a \alert{precise cost
158        model} for the source program
159  \item \alert{certify} the compiler
160  \item embed the compiler in a \alert{prototypical environment} for
161   \begin{itemize}
162    \item stating \alert{cost invariants} based on the inferred cost model
163    \item computing \alert{proof obligations}
164    \item \alert{proving} automatically or interactively the generated proof obligations
165   \end{itemize}
166  \item lift the technique to a \alert{synchronous languaged} (e.g. Esterel)
167        compiled via C
168 \end{enumerate}
169\end{frame}
170
171\begin{frame}
172 \frametitle{CerCo interaction diagram}
173 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
174\end{frame}
175
176\begin{frame}[fragile]
177 \frametitle{Source code}
178\begin{Verbatim}[commandchars=\\\{\}]
179char search (char tab[], char size, char to_find) \{
180  char low = 0, high = size-1, i;
181
182  while (high >= low) \{
183    i = (high+low) / 2;
184    if (tab[i] == to_find) return i;
185
186    if (tab[i] > to_find) high = i-1;
187
188    if (tab[i] < to_find) low = i+1;
189
190  \}
191
192  return (-1);
193\}
194\end{Verbatim}
195\end{frame}
196
197\begin{frame}[fragile]
198 \frametitle{Instrumented source code}
199\begin{Verbatim}[commandchars=\\\{\}]
200char search (char tab[], char size, char to_find) \{
201  char low = 0, high = size-1, i;
202  \alert{cost_incr(117);}
203  while (high >= low) \{
204    \alert{cost_incr(77);}
205    i = (high+low) / 2;
206    if (tab[i] == to_find) \{\alert{cost_incr(30);} return i;\}
207    \alert{else cost_incr(103);}
208    if (tab[i] > to_find) \{\alert{cost_incr(98);} high = i-1;\}
209    \alert{else cost_incr(85);}
210    if (tab[i] < to_find) \{\alert{cost_incr(98);} low = i+1;\}
211    \alert{else cost_incr(88);}
212  \}
213  \alert{cost_incr(43);}
214  return (-1);
215\}
216\end{Verbatim}
217\end{frame}
218
219\begin{frame}[fragile]
220 \frametitle{Foreseen problems}
221 \begin{itemize}
222  \item The \alert{high level implicit control structures}
223    (e.g. missing \texttt{else}) must be made explicit
224  \item Additional \alert{low level control structures} must be made explicit\\
225    (e.g. add low bytes; if overflow then add high bytes)\\
226    Alternative: loss of precision
227  \item The \alert{guards} of the low level control structures could be
228    \alert{``unrelated''} to the high level data\\
229    (e.g. if the carry bit is set then \ldots else \ldots)
230  \item Optimizations can \alert{modify the control flow}\\
231    (e.g. loop hoisting and unrolling)
232  \item The cost can depend on the data manipulated (\alert{dependent annotations}) (e.g. shift, multiplication in simple microprocessors)
233  \item Precise information on the source code required to avoid total
234    alteration (e.g. comments)
235 \end{itemize}
236\end{frame}
237
238\begin{frame}[fragile]
239 \frametitle{Foreseen problems}
240 Strategy in CerCo:
241 \begin{enumerate}
242  \item We consider \alert{simple optimizations} that do not alter the control
243    flow (cfr. CompCert)\\
244    The study of control flow altering optimizations left as optional
245  \item Complex low level control flows \alert{encapsulated} in library
246    functions (if possible) or else \alert{precision loss} (not required yet)
247  \item \alert{Partial alteration of the source program} for justified reasons
248    (e.g. explicit CFs) and for temporary ones (reusal of the CIL suite)\\
249    \alert{To be refined in the next periods}
250 \end{enumerate}
251\end{frame}
252
253\begin{frame}[fragile]
254 \frametitle{Cost invariants: loose invariants}
255{\small
256\begin{Verbatim}[commandchars=\\\{\}]
257char search (char tab[], char size, char to_find) \{
258  char low = 0, high = size-1, i;
259  cost_incr(117);
260  \alert{/* @ label L}
261     \alert{@ invariant cost <= at(cost,L) +}
262      \alert{(77+103+98+88)*((at(high,L) - at(low,L))/(high - low))-1) */}
263  while (high >= low) \{
264    cost_incr(\alert{77});
265    i = (high+low) / 2;
266    if (tab[i] == to_find) \{cost_incr(\alert{30}); return i;\}
267    else cost_incr(\alert{103});
268    if (tab[i] > to_find) \{cost_incr(\alert{98}); high = i-1;\}
269    else cost_incr(\alert{85});
270    if (tab[i] < to_find) \{cost_incr(\alert{98}); low = i+1;\}
271    else cost_incr(\alert{88});
272  \}
273  cost_incr(43);
274  return (-1);
275\}
276\end{Verbatim}
277}
278\end{frame}
279
280\begin{frame}[fragile]
281 \frametitle{Cost invariants: precise invariants}
282 When needed the \alert{user} can also state a precise invariant:
283 \begin{Verbatim}[commandchars=\\\{\}]
284 \alert{cost = at(cost,L) +}
285   \alert{(77 + 103 + 98 + 85) * min(0,#iterations - 1) +}
286   \alert{if tab[(high+low)/2] == to_find then 30 else 103 +}
287   \alert{3 * #high_decremented}
288 \end{Verbatim}
289 where \verb+#high_decremented+ has a complex description.\\~\\
290
291 The more precise the invariant, the more knowledge is required on the
292 extensional semantics of the program.
293\end{frame}
294
295\begin{frame}[fragile]
296 \frametitle{Proof obligations for costs}
297 \alert{Proof obligations} are then generated from the cost invariants using standard
298 techniques (e.g. Weakest Precondition generators for Hoare logic)\\~\\
299
300 \begin{itemize}
301  \item Can use off-the-shelf WP generators
302  \item Ad-hoc tactics/proof strategies to handle the proof obligations will
303        probably help
304 \end{itemize}
305\end{frame}
306
307\begin{frame}
308 \frametitle{Other cost obligations}
309 The same technique applies to: space (stack, heap), energy, etc.\\~\\
310
311 But
312 \begin{center}
313   \alert{\Large space constraints have an effect on the\\extensional semantics too}\end{center}
314
315 Similarly
316 \begin{center}
317   \alert{\Large time constraints have an effect on the\\extensional semantics too when\\considering timers or I/O}\end{center}
318\end{frame}
319
320\begin{frame}
321 \frametitle{Other cost obligations and embedded systems}
322 In CerCo \alert{we have not committed} to other kinds of costs but time.\\~\\
323
324 \alert{Embedded and reactive systems} could greatly benefit from space
325 constraints and from time in presence of timers.\\~\\
326
327 Compatibly with the project timing and effort required, we would like to
328 experiment with other costs too.\\~\\
329
330 Otherwise, this will be left to \alert{future work}.
331\end{frame}
332
333\begin{frame}
334 \frametitle{Case study interaction diagram}
335 \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
336\end{frame}
337
338\section{Project context}
339
340\begin{frame}
341 \frametitle{Related work}
342 \alert{Invariant generation} (also for termination)
343 \begin{itemize}
344  \item Automatic and assisted invariant discovery plays a \alert{central role}
345    for the long term objectives
346  \item Existing techniques are \alert{fully orthogonal} to CerCo: we provide
347    a realistic and precise cost model to be used for cost invariants
348  \item CerCo will \alert{guarantee} that the inferred intensional properties
349    will \alert{carry over to assembly code}
350 \end{itemize}
351\end{frame}
352
353\begin{frame}
354 \frametitle{Related work}
355 \alert{Worst Case Execution Time}
356 \begin{itemize}
357  \item Sophisticated techniques for computing approximate costs of
358    object code programs
359  \item Can target modern architectures (caches, pipelines, reordering of
360    instructions, \ldots) using \alert{static (precise) or dinamic (empyrical)
361    techniques}
362  \item Main problem: \alert{how to relate} analysis on object code to the
363    intermediate and source languages and \alert{how to trust} the results
364  \item In CerCo:
365   \begin{enumerate}
366    \item Costs are tightly related by designing \alert{compilers} with this aim
367     (cfr. wcc)
368    \item WCET computations are \alert{certified}
369    \item \alert{Interactivity} vs full automation
370   \end{enumerate}
371  \item CerCo will target only a simple architecture;\\ \alert{combination} with
372    (dynamic?) WCET \alert{necessary}\\ in the long term
373 \end{itemize}
374\end{frame}
375
376\begin{frame}
377 \frametitle{Related work}
378 \alert{Compiler certification and interactive theorem proving}
379 \begin{itemize}
380  \item A large and older litterature that focuses on \alert{academic examples}
381  \item Some impressive recent examples that targets \alert{realistic
382    mildly optimizing compilers} (e.g. CompCert, FR)
383  \item On-going projects that targets more \alert{complex scenarios}:
384    intensional properties (CerCo, EU), whole software/hardware
385    architectures (e.g. VeriSoft, DE), concurrent systems (USA),
386    higher level languages, \ldots
387 \end{itemize}
388\end{frame}
389
390\section{Project planning and achievements}
391
392\begin{frame}
393 \includegraphics[height=8cm]{figs/pert.pdf}
394\end{frame}
395
396\begin{frame}
397 \frametitle{Achievements (1st period)}
398 Main theoretical achievements (D2.1):
399 \begin{center}
400  \alert{\Large a methodology for lifting in a provably correct way
401    costs on the object code to costs in the source code}
402 \end{center}~\\
403
404 Main practical achievements (D2.2):
405 \begin{center}
406  \alert{\Large an untrusted compiler from C-Light to the MCS-51 microprocessor
407   that lifts costs on the object code to costs in the source code}
408 \end{center}
409\end{frame}
410
411\begin{frame}
412 \frametitle{Achievements (1st period)}
413 More in detail:
414 \begin{enumerate}
415  \item The \alert{methodology itself}, with comparison with an alternative proposal (D2.1).  Main issues:
416   \begin{enumerate}
417    \item meaning of cost annotations
418    \item method to prove them sound and precise
419    \item \alert{compositionality}
420   \end{enumerate}
421  \item Assessment of the methodology: formalization of a \alert{toy compiler in Coq}
422  \item First untrusted prototype from C-Light to Mips
423  \item Full \alert{formalization} in O'Caml of the \alert{MCS-51} ``environment'':
424    \begin{enumerate}
425     \item ALU
426     \item UART, I/O lines, timers, interrupts
427     \item an assembly language with pseudo-instructions +\\ an assembler
428     \item an Intel HEX parser/pretty printer
429    \end{enumerate}
430 \end{enumerate}
431\end{frame}
432
433\begin{frame}
434 \frametitle{Achievements (1st period)}
435 More in detail:
436 \begin{enumerate}
437  \item \alert{Partial assessment} of the MCS-51 O'Caml formalization
438  \item \alert{Extension of C}, the CIL suite and the CompCert
439    \alert{memory model} to the MCS-51 unorthogonal memory model (new type and
440    pointer modifiers taken from SDCC)
441  \item \alert{Partial porting} of the CerCo untrusted prototype to the
442    MCS-51 and to the extended C
443  \item \alert{Partial porting} of the MCS-51 O'Caml formalization to Matita\\
444        The formalization is directly executable
445  \item \alert{Formalization} in Matita of the \alert{extended C-Light version}\\
446        The formalization is directly \alert{executable}
447  \item \alert{Partial assessment} of the executable semantics by
448        proving it equivalent to the CompCert one (up to extensions)
449 \end{enumerate}
450\end{frame}
451
452\begin{frame}
453 \frametitle{Assessment}
454 Assessment level and strategies:
455 \begin{enumerate}
456  \item Untrusted CerCo compiler (D2.2, M1):\\
457    the compiler will be \alert{fully certified};
458    several bugs already found after
459    the release of the deliverables
460  \item MCS-51 model (D4.1):\\
461    \alert{more thorough testing} vs emulators and real processors is
462    required;\\
463    minor impact on the rest of the projects;\\
464    the assembler will be certified (some bugs already found + unimplemented
465    features)
466  \item extended C semantics (D3.1):\\
467    already \alert{proved to be equivalent} to the CompCert one
468    (up to extensions);\\
469    we do not commit to support the planned extensions
470 \end{enumerate}
471\end{frame}
472
473\begin{frame}
474 \frametitle{Deviations from DoW}
475 \alert{Minor deviations} from the DoW
476 (no significant impact on the future schedule):
477 \begin{enumerate}
478  \item Late delivery of the deliverable related to the Web site and
479    internal work-flow due to hardware problems. \alert{Solved}
480  \item Compiler prototype D2.2 (M1):\\
481    computation of realistic costs requires full integration with D4.1
482    (not completed/tested at release time) \alert{Solved}
483  \item MCS-51 memory model + C extensions:\\
484    we did not foresee the need of MCS-51 specific extensions;\\
485    they will be taken in account with low priority\\
486    at the moment, only partially implemented in a branch of D2.2
487    not ready for release. \alert{Under consideration}
488 \end{enumerate}
489\end{frame}
490
491\begin{frame}
492 \frametitle{Foreseen deviations from DoW}
493 All sites have faced different hiring problems.\\~\\
494
495  UNIBO (Project Coordinator).\\
496   \alert{Personel planned:} 1 post-doc (24m) + 1 RTD (non permanent researcher) 24m\\
497   \alert{Personel acquired:} 1 post-doc (24m)\\
498   \alert{Cause:}
499   Because of the reform of the Italian University it has not been possible
500   to hire a RTD yet and it is unlikely to be possible to hire him soon.\\
501   \alert{Solution:} in place of the RTD, we will acquire two post-docs
502   (24m + 18m) that will start later then expected and will have a lower
503   level of expertise. Both positions are still waiting for clarifications
504   from the ministry or approval from the Corte dei Conti.\\
505   \alert{Expected impact:} delivery of D4.2 (month 18) could\\
506   be delayed with no impact on the next milestone\\
507   (M2, month 24), potential impact on M3, month 36.
508\end{frame}
509
510\begin{frame}
511 \hspace{-5cm}
512 \includegraphics[height=8cm]{figs/pert.pdf}
513\end{frame}
514
515\begin{frame}
516 \frametitle{Foreseen deviations from DoW}
517 All sites have faced different hiring problems.\\~\\
518
519  UPD.\\
520   \alert{Personel planned:} 1 post-doc (12m) + 1 PhD student (36m) + master students\\
521   \alert{Personel acquired:} 1 post-doc (12m) + 1 phd student (6m) + 2 master students\\
522   \alert{Cause:}
523    After 6 months of work the PhD student has decided to resign.
524    At this point, it is neither possible (incomplete funding)
525    nor desirable (bootstrapping period) to look for another PhD
526    student.\\
527   \alert{Solution:}
528    We plan --- if possible --- to extend as much as
529    possible the post-doc to cover also the second and/or third period.\\
530   \alert{Expected impact:} no major expected impact.
531\end{frame}
532
533\begin{frame}
534 \frametitle{Foreseen deviations from DoW}
535 All sites have faced different hiring problems.\\~\\
536
537  UEDIN.\\
538   \alert{Personel planned:} 1 lecturer (36m) + 1 post-doc (36m) + 1 phd-student \\
539   \alert{Personel acquired:} 1 lecturer (14m) + Senior lecturer (24m) + 1 post-doc
540   \alert{Cause:}
541    Dr. Randy Pollack (former site leader) is moving to Harvard.
542    He will be employed 90\% of his time there and 10\% on CerCo at UEDIN.
543    Dr. Ian Stark is the new site leader (since 01 February).
544    No student with appropriate background was found.\\
545   \alert{Solution:}
546    We plan to hire a post-doc during the later part of the project to
547    compensate for the missing PhD student.\\
548   \alert{Expected impact:} some trading of person-months between projects
549    and reassignment of costs: an experienced researcher will be more expensive
550    than a PhD student, but could reasonably expect to carry out the formal
551    proof work in less time than a student.
552\end{frame}
553
554\section{Project management}
555
556\begin{frame}
557 \frametitle{The Project at a Glance}
558 \begin{tabular}{ll}
559 Title: & Certified Complexity \\
560 Acronym: & CerCo \\
561 Research Area: & ICT-2007.8.0 FET Open \\
562 \alert{Number of Partners:} & \alert{3} \\
563 Grant Agreement N. & 243881 (13/11/2009) \\
564 %Proposal Contract N. & \\
565 Oper. Commenc. Date: & 01/02/2010 \\ 
566 \alert{Duration}: & \alert{36 months} \\
567 Project Cost: & $\geq$ 1,520,000 \euro \\
568 Budget: & ~~~~1,164,533 \euro \\
569 Pre-Financing: & ~~~~~~~621,084 \euro \\
570 \alert{Reporting Periods:} & \alert{1--12}, 13--24, 25--36 \\
571 \end{tabular}
572\end{frame}
573
574\begin{frame}
575 \frametitle{The Partnership at a Glance}
576  \alert{UNIBO (ALMA Mater Studiorum, Universit\'a di Bologna)}\\
577  79 m.m., 473,040 \euro, Coordinator\\
578
579   \begin{itemize}
580    \item Claudio Sacerdoti Coen (project leader)\\
581          (Permanent Researcher)
582    \item Michela Cozzi (project management team) (Administrative)
583    \item Andrea Asperti (Full Professor)
584    \item Dominic Mulligan (Post-Doc)
585    \item Two Post-Doc to be hired
586    \item PhD. Students: Wilmer Ricciotti
587    \item Undergraduate/Master Students: Cosimo Arndt Oliboni
588   \end{itemize}
589\end{frame}
590
591\begin{frame}
592 \frametitle{The Partnership at a Glance}
593  \alert{UPD (Universit\'e Paris Diderot - Paris VII)}\\ 66 m.m., 314,457 \euro\\
594 \begin{itemize}
595  \item Roberto Amadio (site leader) (Full Professor)
596  \item Yann R\'egis-Gianas (Maitre de Conference)
597  \item Nicolas Ayache (Post-Doc)
598  \item Ronan Saillard (Internship + PhD student)
599  \item Kayvan Memarian (Internship)
600 \end{itemize}
601\end{frame}
602
603\begin{frame}
604 \frametitle{The Partnership at a Glance}
605  \alert{UEDIN (University of Edinburgh)}\\ 69 m.m., 377,036 \euro\\
606 \begin{itemize}
607  \item Ian Stark (site leader), (Senior Lecturer)
608  \item Randy Pollack (former site leader), (Senior Research Fellow)
609  \item Brian Campbell (Post-Doc)
610  \item One Post-Doc to be hired
611 \end{itemize}
612\end{frame}
613
614\begin{frame}
615 \frametitle{Management activities}
616 Management WP1:
617 \begin{enumerate}
618  \item to \alert{coordinate and supervise} activities to be
619    carried out
620  \item to carry out the overall \alert{administrative and
621    financial management} of the project
622  \item to manage \alert{contacts with the European Commission}
623  \item to \alert{monitor quality and timing} of project deliverables
624  \item to establish effective internal and external
625        \alert{communication procedures}
626 \end{enumerate}
627\end{frame}
628
629\begin{frame}
630 \frametitle{Consortium structure}
631 \includegraphics[height=8cm]{figs/management.pdf}
632\end{frame}
633
634\begin{frame}
635 \frametitle{Finantial management and coordination}
636 During first period:
637 \begin{enumerate}
638  \item transmission \alert{pre-financing} to all beneficiaries
639  \item \alert{providing} to partners detailed \alert{information} on consortium
640    organization and FP7 management rules during Kick Off
641  \item \alert{collecting and checking} partner's \alert{financial information} for the
642    First Progress Report
643  \item \alert{submission of financial statement} through NEF system (in progress)
644  \item gathering all necessary information and submission of \alert{management
645   reports, activity reports and deliverables}
646 \end{enumerate}
647\end{frame}
648
649\begin{frame}
650 \frametitle{Consortium agreement}
651 \begin{itemize}
652  \item signed in \alert{January 2010}
653  \item Intellectual Property Rights, Access Rights, roles,
654    functioning and responsibilities of governing bodies, liability of the
655    partners
656 \end{itemize}
657\end{frame}
658
659\begin{frame}
660 \frametitle{Periodic Meetings}
661 Four project meetings during first period (two planned in the DoW):
662 \begin{itemize}
663  \item \alert{Kick-off, Bologna, February 2010.}\\
664   coordination of research activities, planning of future work,
665   financial and administrative organization
666  \item \alert{Project meeting, Edinburgh, July 2010.}\\
667   Just after D2.1. Fixing more precise scheduling; first informal
668   dissemination via co-location with FLOC
669  \item \alert{Project meeting, Paris, Septermber 2010.}\\
670   Adoption of the MCS-51 target; discussion of the design of the costing
671   compiler (D2.2), memory model (D4.1). Integration problems foreseen.
672  \item \alert{Implementer's meeting, Bologna, January 2011}\\
673   Addressing remaining integration problems regarding\\ D2.2, D3.1 and D4.1.
674   Post-poning some integration\\ steps to Task 2.4 (second period).
675 \end{itemize}
676\end{frame}
677
678\end{document}
Note: See TracBrowser for help on using the repository browser.