Changeset 1848


Ignore:
Timestamp:
Mar 15, 2012, 3:17:59 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/Presentations/WP1-claudio.tex

    r1838 r1848  
    121121 \alert{We started with a simple scenario:}
    122122 \begin{itemize}
    123   \item Simple compilation model (no changes to the control flow)
    124   \item Trivial hardware model
    125  \end{itemize}
    126 
    127  \alert{We will formally certify the trivial scenario}\\~\\
     123  \item Conventional compilation model without changes to the control flow
     124  \item Deterministic widely deployed hardware model (no caching, pipelining)
     125 \end{itemize}
     126
     127 \alert{We will formally certify the simple scenario}\\~\\
    128128
    129129 \alert{We have started to scale to most complex scenarios\\
     
    228228 \alert{serious loss of precision} (if we take the maximum cost).
    229229
    230  Solution imagined at the previous review:\\
     230 Solution sketched at the previous review:\\
    231231 \alert{dependent costs: the cost is a function of the state}
    232232\end{frame}
     
    248248 \alert{serious loss of precision} (if we take the maximum cost).
    249249
    250  Solution imagined at the previous review:\\
     250 Solution sketched at the previous review:\\
    251251 \alert{dependent costs: the cost is a function of the state}
    252252\end{frame}
     
    290290\begin{frame}
    291291 \frametitle{Recommendations from the reviewers: action taken}
    292  Impact on the project planning:\\~\\
    293 
     292 \alert{No impact on planning}\\
    294293 Dr. Tranquilli and Dr. Boender (Post-Docs) were hired by UNIBO in place of the
    295294 senior researcher whose hiring was made impossible during the first period.\\
    296295 ~\\
    297296
    298  No impact on the budget\\
     297 \alert{No impact on budget}\\
    299298 Minor delays so far on the project plan (Dr. Boender alone is less experienced
    300299 than the originally expected candidate)\\
     
    311310\begin{frame}
    312311 \frametitle{Recommendations from the reviewers}
    313  Approach surely feasible and already followed in the EmBounded EU Project:
    314  \begin{itemize}
    315   \item the compiler informs the WCET tool about high level constraints on the
    316    control flow
    317   \item the WCET tool performs a fine grained analysis (e.g. by total unrolling
    318    the loops) assuming a given processor state (e.g. empty cache)
    319   \item the WCET tool abstracts the analysis to a number (the bound,
    320    independent from the program status) that is returned
    321   \item additional code must be generated to put the processor in the assumed
    322    state to avoid caching anomalies
    323  \end{itemize}
    324 \end{frame}
    325 
    326 \begin{frame}
    327  \frametitle{Recommendations from the reviewers}
    328  Comparison with dependent labelling:\\~\\
    329 
    330   Dependent labelling does not use WCET tools as black-boxes;\\
    331   it tightly integrates with WCET tools
    332    \begin{itemize}
    333     \item Pro: processor state exchanged in input/output, no need for a fixed
    334      input state $\Rightarrow$ better precision
    335     \item Pro: all details of the analysis exploited (instead of abstracting
    336      to a single bound) $\Rightarrow$ better precision
    337     \item Pro: it follows the interactive theorem proving perspective
    338      (abstraction/automation are performed later)
    339     \item Cons: require a re-implementation/modification of existing WCET
    340      tools
    341    \end{itemize}
     312 Suggested approach (EmBounded):
     313 \begin{itemize}
     314  \item \alert{Chunks} fed to the WCET tool and analyzed \alert{in isolation}
     315  \item In isolation processor \alert{state unknown}
     316        $\Rightarrow$ \alert{loss of precision}
     317  \item Result of the analysis abstracted to \alert{one number} per chunk
     318 \end{itemize}
     319 Dependent labelling approach (\alert{CerCo}):
     320 \begin{itemize}
     321  \item \alert{Global analysis} of the object code
     322        $\Rightarrow$ improved precision
     323  \item Result of the analysis exposed via \alert{dependent costs}\\
     324        $\Rightarrow$ \alert{improved precision}
     325 \end{itemize}
    342326\end{frame}
    343327
    344328\begin{frame}
    345329 \frametitle{Recommendations from the reviewers: action taken}
    346  We plan to continue the study of dependent labelling to accomodate caches.\\~\\
    347 
    348  We will follow the reviewer's suggestion only as last resort in case of
    349  failure.
     330 Plan: to apply dependent labelling to caches.\\~\\
     331
     332 Reviewer's suggestion available as a fallback.
    350333\end{frame}
    351334
     
    358341 Done.
    359342 \begin{itemize}
    360   \item A major issue with the proof plan has been found.\\
    361         The issue was not there for the toy compiler and thus went unnoticed.\\
    362         Solved introducing \emph{structured traces}.
    363   \item The overall effort required is consistent with the men-months allocated
    364         to the project.
    365   \item The estimation is based on our perception of the proof complexity and
    366         on projections obtained from code size and coefficients computed
     343  \item This made explicit the need to consider \emph{structured traces}.\\
     344        Not needed in the proof of the toy compiler.
     345  \item The overall \alert{effort} required is \alert{consistent} with the
     346        person-months allocated to the project.
     347  \item The estimation is based on our \alert{judgement of the proof complexity} and on \alert{projections} obtained from code size and coefficients computed
    367348        from CompCert.
     349 \end{itemize}
     350\end{frame}
     351
     352\begin{frame}
     353 \frametitle{Recommendations from the reviewers}
     354 ``Based on the outline of the paper-and-pencil proofs, the authors should
     355 estimate the effort for two possible scenarios: a) proceed as planned in the
     356 Matita system (this involves porting all proofs of the CompCert project to
     357 Matita); b) modify the existing proofs in Coq\ldots If the project partners
     358 stick to the usage of Matita they should argue convincingly why this is a
     359 suitable choice and in how far Matita is superior to Coq\ldots''
     360\end{frame}
     361
     362\begin{frame}
     363 \frametitle{Recommendations from the reviewers: action taken}
     364 \begin{enumerate}
     365  \item Misconception: we \alert{do not} want to port/reuse CompCert proofs;
     366        in any case CompCert \alert{licensing forbids} this
     367  \item CerCo is first of all a project in certified compiler verification.
     368   \alert{Comparing design alternatives is a key scientific contribution}\\~\\
     369
     370   \begin{tabular}{lll}
     371     & CerCo & CompCert \\
     372    Semantics & executable & inductive \\
     373    Proofs     & computed proof obligations & traditional \\
     374    Types      & dependent & ML \\
     375    Datatypes  & graphs & lists \\
     376    Semantics  & read-only program + pc & small step operational \\
     377   \end{tabular}
     378 \end{enumerate}
     379\end{frame}
     380
     381\begin{frame}
     382 \frametitle{Recommendations from the reviewers: action taken}
     383 \begin{enumerate}
     384  \item Commitment to the \alert{promotion of Matita}.
     385  \item Exploiting implementation differences\\~\\
     386   \begin{tabular}{lll}
     387       & Matita & Coq \\
     388    Small scale automation & unification hints & type classes \\
     389    Big scale automation   & paramodulation & resolution \\
     390    Tactics                & tinycals & LCF \\
     391    Specifications         & executable & relational \\
     392   \end{tabular}\\~\\
     393  \item \alert{Co-development}:
     394    when you have control of the tool, you can adapt the tool
     395    instead of adapting the formalization
     396 \end{enumerate}
     397 Because of the previous motivations and the positive\\ outcome
     398 of the effort estimation, \alert{we stick to original plan}.
     399\end{frame}
     400
     401\section{Project planning and achievements}
     402
     403\begin{frame}
     404 \includegraphics[height=8cm]{figs/pert.pdf}
     405\end{frame}
     406
     407\begin{frame}
     408 \frametitle{Achievements (2nd period) 1/3, Ayache's talk}
     409 From the \alert{CerCo annotating compiler} (1st period)\\
     410 ~~~~~ - inference of costs for basic blocks;\\
     411 ~~~~~ - instrumentation of the source code\\
     412 to the \alert{CerCo untrusted prototype} (2nd period)\\
     413 ~~~~~ - inference of cost invariants;\\
     414 ~~~~~ - certified proofs of cost obligations;\\
     415 \begin{enumerate}
     416  \item Integration of the CerCo compiler into \alert{Frama-C} (D5.1)
     417   \item The abstract interpretation based \alert{Frama-C CerCo plug-in} for
     418     the inference of \alert{global complexity assertions} (D5.1)
     419   \item The \alert{Lustre CerCo plug-in} for
     420     automated analysis of WCRT (D5.3)
     421 \end{enumerate}
     422\end{frame}
     423
     424\begin{frame}
     425 \frametitle{CerCo interaction diagram}
     426 \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
     427\end{frame}
     428
     429\begin{frame}
     430 \frametitle{Achievements (2nd period) 2/3, Mulligan/Campbell talks}
     431 Towards the \alert{CerCo trusted prototype} (3rd period)\\
     432 ~~~ - to verify preservation of labelled traces;\\
     433 ~~~ - to verify exact correspondence between actual and inferred\\
     434 ~~~   execution cost\\
     435 \begin{enumerate}
     436  \item CIC encoding: Front/Back end (D4.2/D4.3)
     437  \item \mbox{\rlap{Executable semantics of all intermediate languages (D3.3/D4.3)}}
     438  \item Beginning of formal verification
     439   \begin{itemize}
     440    \item Common/generic definitions, \alert{data structures} to represent invariants,
     441          \alert{invariants} enforced as dependent types
     442    \item \alert{Optimizing assembler} verification (75\%)
     443    \item Proof of \alert{correspondence} of actual and inferred cost (95\%)
     444    \item Generation of \alert{structured} labelled traces (for the\\
     445          back-end) from \alert{flat} labelled traces (from the\\ front-end)
     446   \end{itemize}
     447 \end{enumerate}
     448\end{frame}
     449
     450\begin{frame}
     451 \frametitle{Achievements (2nd period) 3/3 R\`egis-Gianas/Tranquilli talks }
     452 \alert{Enlarging the scope} of CerCo techniques
     453 \begin{enumerate}
     454  \item Extension of the basic labelling approach to cover \alert{functional
     455   languages} (D5.1)\\
     456   - prototype implemented
     457  \item Dependent labelling approach to cover \alert{control flow alterations}
     458   and \alert{modern hardware features} (D5.1)\\
     459   - branch of CerCo compiler with loop optimizations, redundancy elimination,
     460     etc.
     461 \end{enumerate}
     462\end{frame}
     463
     464\begin{frame}
     465 \frametitle{Assessment}
     466 Assessment level and strategies:
     467 \begin{enumerate}
     468  \item CIC encoding: Front/Back end (D4.2/D4.3):\\
     469    - \alert{tested} inside Matita (executable code);\\
     470    - to be \alert{certified} in D3.4/D4.4 (Front/Back end correctness)
     471  \item \makebox[0pt][l]{Executable semantics of intermediate languages
     472    (D3.3/D4.3):}\\
     473    \alert{tested} by executing programs
     474  \item Untrusted CerCo prototype (D5.1, M2):\\
     475    - tested (methodology + code) in the \alert{case study} (D5.3);\\
     476    - plan to test on library of cryptographic functions
     477  \item Case study: analysis of synchronous code (D5.3):\\
     478   - \alert{self testing code} checks correctness and precision\\
     479   - tested on examples
     480 \end{enumerate}
     481\end{frame}
     482
     483\begin{frame}
     484 \frametitle{Deviations from DoW}
     485 \alert{Minor deviations} from the DoW
     486 (no significant impact on the future schedule):
     487 \begin{enumerate}
     488  \item At month 16 (+16): submission of the commitment letter and
     489    addenda required by the reviewers. \alert{Done}
     490  \item Late delivery of D4.2 delayed D3.2, D3.3, D4.3 (at month 21, planned
     491    at month 18).\\ Bologna: one post-doc in place of senior researcher
     492    (plus another on dependent labelling).\\
     493    \alert{No short term impact, possible minor impact at month 36}
     494 \end{enumerate}
     495\end{frame}
     496
     497\begin{frame}
     498 \hspace{-5cm}
     499 \includegraphics[height=8cm]{figs/pert.pdf}
     500\end{frame}
     501
     502\begin{frame}
     503 \frametitle{Deviations from DoW}
     504 \alert{Major deviations} from the DoW
     505 \begin{enumerate}
     506  \item Research on dependent labelling in response to reviewers.\\
     507    \alert{No impact on the schedule, work performed by additional Post-Doc.}
     508  \item Bring forward D5.3 from the third to the second period.\\
     509    D5.3 is a major case study to assess the potential
     510    of CerCo technology $\Rightarrow$ \alert{early dissemination}.\\
     511    Enabled by replacement of PhD student by Post-Doc in Paris\\~\\
     512    {\Large \alert{We hereby officially require permission for\\
     513    early delivery of D5.3 in second period}}
     514 \end{enumerate}
     515\end{frame}
     516
     517\begin{frame}
     518 \hspace{-5cm}
     519 \includegraphics[height=8cm]{figs/pert.pdf}
     520\end{frame}
     521
     522\section{Project management}
     523
     524\begin{frame}
     525 \frametitle{Management activities}
     526 Management WP1:
     527 \begin{enumerate}
     528  \item to \alert{coordinate and supervise} activities to be
     529    carried out
     530  \item to carry out the overall \alert{administrative and
     531    financial management} of the project
     532  \item to manage \alert{contacts with the European Commission}
     533  \item to \alert{monitor quality and timing} of project deliverables
     534  \item to establish effective internal and external
     535        \alert{communication procedures}
     536 \end{enumerate}
     537\end{frame}
     538
     539\begin{frame}
     540 \frametitle{Financial management and coordination}
     541 During second period:
     542 \begin{enumerate}
     543  \item transmission \alert{pre-financing} to all beneficiaries
     544  \item \alert{collecting and checking} partner's \alert{financial information} for the
     545    Second Progress Report
     546  \item \alert{submission of financial statement} through NEF system (in progress)
     547  \item gathering all necessary information and submission of \alert{management
     548   reports, activity reports and deliverables}
     549 \end{enumerate}
     550\end{frame}
     551
     552\begin{frame}
     553 \frametitle{Periodic Meetings}
     554 Three project meetings during 2nd period (one planned in DoW):
     555 \begin{itemize}
     556  \item Project meeting, Edinburgh, February 2011.\\
     557   %Planning; review of decisions taken during implementor's meeting, discussion on the proof strategy and on the actions to be taken as an answer to the reviewer's recommendations.
     558  \item Project meeting, Paris, September 2011.\\
     559   \alert{Federated CerCo and Eternal meeting}
     560   %(for dissemination and to establish co-operation). Review of deliverables due at month 18. Invited speaker from WCET community.
     561  \item Implementer's meeting, Edinburgh, November 2011\\
     562   %Discussion of issues found in the global proof strategy; introduction of the notion of structured traces and re-planning of the global proof strategy. Integration problems\\ addressed.
    368563 \end{itemize}
    369564\end{frame}
     
    392587\end{frame}
    393588
    394 \begin{frame}
    395  \frametitle{Recommendations from the reviewers}
    396  ``Based on the outline of the paper-and-pencil proofs, the authors should
    397  estimate the effort for two possible scenarios: a) proceed as planned in the
    398  Matita system (this involves porting all proofs of the CompCert project to
    399  Matita); b) modify the existing proofs in Coq\ldots If the project partners
    400  stick to the usage of Matita they should argue convincingly why this is a
    401  suitable choice and in how far Matita is superior to Coq\ldots''
    402 \end{frame}
    403 
    404 \begin{frame}
    405  \frametitle{Recommendations from the reviewers: action taken}
    406  \begin{enumerate}
    407   \item CompCert proofs are not open source; the proposal was aiming to
    408    a realistic mildly optimizing open source compiler
    409   \item CerCo is first of all a project in certified compiler verification.
    410    We wanted to experiment with different design choices
    411    \begin{itemize}
    412     \item Executable (CerCo) vs non executable (CompCert) semantics
    413     \item Russell (Program) style proofs (CerCo) vs inductive reasoning (CompCert)
    414     \item Dependent types (CerCo) vs simple (ML) types (CompCert)
    415     \item Different program representations: graphs (Cerco) vs linear (CompCert)
    416     \item Different semantics: read-only program + pc (CerCo) vs small operational semantics (CompCert)
    417     \item Different back-ends (order of passes, etc.)
    418    \end{itemize}
    419   We do not claim to be always better: we want to\\ compare.
    420  \end{enumerate}
    421 \end{frame}
    422 
    423 \begin{frame}
    424  \frametitle{Recommendations from the reviewers: action taken}
    425  \begin{enumerate}
    426   \item One partner really interested in the promotion and co-development
    427     of Matita.\\
    428     Coq and Matita are incomparable (not clones). Examples:
    429    \begin{itemize}
    430     \item Type classes (Coq) vs unification hints (Matita)
    431     \item Different tactic language: LCF (Coq) vs tinycals (Matita)
    432     \item Different automation: ad-hoc (Coq) vs paramodulation based (Matita)
    433     \item Coq favors inductive types, Matita executable definitions
    434    \end{itemize}
    435   \item Co-development:
    436     When you have control of the tool, you can adapt the tool
    437     instead of adapting the formalization
    438  \end{enumerate}
    439  Because of the previous motivations and the positive outcome (feasibility)
    440  of the effort estimation, \alert{we keep following\\ the original plan}.
    441 \end{frame}
    442 
    443 \section{Project planning and achievements}
    444 
    445 \begin{frame}
    446  \includegraphics[height=8cm]{figs/pert.pdf}
    447 \end{frame}
    448 
    449 \begin{frame}
    450  \frametitle{Achievements (2nd period)}
    451  From the \alert{CerCo annotating compiler} (1st period)\\
    452  ~~~~~ - inference of costs for basic blocks;\\
    453  ~~~~~ - instrumentation of the source code\\
    454  to the \alert{CerCo untrusted prototype} (2nd period)\\
    455  ~~~~~ - inference of cost invariants;\\
    456  ~~~~~ - certified proofs of cost obligations;\\
    457  \begin{enumerate}
    458   \item Integration of the CerCo compiler into Frama-C to perform
    459     \alert{totally trusted} proofs of intentional properties (D5.1)
    460    \item The Abstract Interpretation based \alert{Frama-C CerCo plug-in} for
    461      the inference of complexity assertions (D5.1)\\
    462      A partially automatic simple but fully trusted WCET analyzer
    463    \item The \alert{Lustre CerCo plug-in} for
    464      the inference of complexity assertions (D5.3)\\
    465      An automatic simple but fully trusted WCRT analyzer
    466  \end{enumerate}
    467 \end{frame}
    468 
    469 \begin{frame}
    470  \frametitle{CerCo interaction diagram}
    471  \includegraphics[height=8cm]{figs/interaction_diagram.pdf}
    472 \end{frame}
    473 
    474 \begin{frame}
    475  \frametitle{Case study interaction diagram}
    476  \includegraphics[height=7cm]{figs/case_study_diagram.pdf}
    477 \end{frame}
    478 
    479 
    480 \begin{frame}
    481  \frametitle{Achievements (2nd period)}
    482  Towards the \alert{CerCo trusted prototype} (3rd period)\\
    483  ~~~~~ - formal verification of the preservation of (structured)\\
    484  ~~~~~ labelled traces;\\
    485  ~~~~~ formal verification of correspondence between the actual\\
    486  ~~~~~ - execution time (of object code) and the one predicted from\\
    487  ~~~~~ (structured) labelled traces (all languages);\\
    488  \begin{enumerate}
    489   \item CIC encoding: Front/Back end (D4.2/D4.3)
    490   \item Executable formal semantics of front/back end intermediate languages
    491     (D3.3/D4.3)
    492   \item Beginning of formal verification
    493    \begin{itemize}
    494     \item Common/generic definitions, data structures to represent invariants,
    495           invariants enforced as dependent types
    496     \item Optimizing assembler verification (75\%)
    497     \item Proof of precise correspondence of real and estimated cost (95\%)
    498     \item Generation of structured labelled traces (for the back-end) from
    499           flat labelled traces (from the front-end)
    500    \end{itemize}
    501  \end{enumerate}
    502 \end{frame}
    503 
    504 \begin{frame}
    505  \frametitle{Achievements (2nd period)}
    506  Enlarging the scope of CerCo techniques
    507  \begin{enumerate}
    508   \item Extension of the basic labelling approach to cover functional
    509    languages (D5.1)\\
    510    - prototype implemented
    511   \item Dependent labelling approach to cover control flow alterations
    512    and modern hardware features (D5.1)\\
    513    - branch of CerCo compiler with loop optimizations, redundancy elimination,
    514      etc.
    515  \end{enumerate}
    516 \end{frame}
    517 
    518 \begin{frame}
    519  \frametitle{Assessment}
    520  Assessment level and strategies:
    521  \begin{enumerate}
    522   \item CIC encoding: Front/Back end (D4.2/D4.3):\\
    523     - tested inside Matita (executable code);\\
    524     - to be certified in D3.4/D4.4 (Front/Back end correctness)
    525   \item Executable formal semantics of front/back end intermediate languages
    526     (D3.3/D4.3):\\
    527     tested by executing programs
    528   \item Untrusted CerCo prototype (D5.1, M2):\\
    529     - tested (methodology + code) in the case study (D5.3);\\
    530     - plan to test on library of cryptographic functions
    531   \item Case study: analysis of syncrhonous code (D5.3):\\
    532    - self testing code to check correctness and estimate\\ precision
    533    - tested on some examples
    534  \end{enumerate}
    535 \end{frame}
    536 
    537 \begin{frame}
    538  \frametitle{Deviations from DoW}
    539  \alert{Minor deviations} from the DoW
    540  (no significant impact on the future schedule):
    541  \begin{enumerate}
    542   \item At month 16 (+16): submission of the commitment letter and
    543     addenda required by the reviewers. \alert{Done}
    544   \item Late delivery of D3.2, D3.3, D4.2, D4.3 (at month 21, planned
    545     at month 18). Bologna hired two Post-Docs in place of a senior
    546     researcher. One Post-Doc allocated to the dependent labelling approach.
    547     The other has a lower level of maturity than expected. Thus we faced
    548     a delay in D4.2 and D4.3 that reflected on D3.2 and D3.3 (for integration).
    549     \alert{No short term impact, possible minor impact at month 36}
    550  \end{enumerate}
    551 \end{frame}
    552 
    553 \begin{frame}
    554  \hspace{-5cm}
    555  \includegraphics[height=8cm]{figs/pert.pdf}
    556 \end{frame}
    557 
    558 \begin{frame}
    559  \frametitle{Deviations from DoW}
    560  \alert{Major deviations} from the DoW
    561  \begin{enumerate}
    562   \item Introduction of the dependent labelling approach and application to
    563     the pen-and-paper proof of a toy compiler. Forking of the CerCo compiler
    564     and Frama-C plug-in to implement loop optimizations and
    565     redundancy elimination.
    566     \alert{No impact on the schedule, work performed by additional Post-Doc.}
    567   \item Anticipation of D5.3 from the third to the second period.
    568     D5.3 is a major case study and its role is that of assessing the potential
    569     of CerCo technology on some restricted scenario. Useful for early
    570     dissemination too. Made possible by hiring problems in Paris (resignation
    571     of PhD student during first period and extension of Post-Doc contract
    572     to cover second period).
    573     \alert{We hereby officially require permission to\\
    574     anticipate delivery of D5.3 to second period}
    575  \end{enumerate}
    576 \end{frame}
    577 
    578 \begin{frame}
    579  \hspace{-5cm}
    580  \includegraphics[height=8cm]{figs/pert.pdf}
    581 \end{frame}
    582 
    583 \section{Project management}
    584 
    585 \begin{frame}
    586  \frametitle{Management activities}
    587  Management WP1:
    588  \begin{enumerate}
    589   \item to \alert{coordinate and supervise} activities to be
    590     carried out
    591   \item to carry out the overall \alert{administrative and
    592     financial management} of the project
    593   \item to manage \alert{contacts with the European Commission}
    594   \item to \alert{monitor quality and timing} of project deliverables
    595   \item to establish effective internal and external
    596         \alert{communication procedures}
    597  \end{enumerate}
    598 \end{frame}
    599 
    600 \begin{frame}
    601  \frametitle{Financial management and coordination}
    602  During first period:
    603  \begin{enumerate}
    604   \item transmission \alert{pre-financing} to all beneficiaries
    605   \item \alert{collecting and checking} partner's \alert{financial information} for the
    606     Second Progress Report
    607   \item \alert{submission of financial statement} through NEF system (in progress)
    608   \item gathering all necessary information and submission of \alert{management
    609    reports, activity reports and deliverables}
    610  \end{enumerate}
    611 \end{frame}
    612 
    613 \begin{frame}
    614  \frametitle{Periodic Meetings}
    615  Three project meetings during 2nd period (one planned in DoW):
    616  \begin{itemize}
    617   \item \alert{Project meeting, Edinburgh, February 2011.}\\
    618    Planning; review of
    619    decisions taken during implementor's meeting, discussion on the
    620    proof strategy and on the actions to be taken as an answer
    621    to the reviewer's recommendations.
    622   \item \alert{Project meeting, Paris, September 2011.}\\
    623    Federated CerCo and Eternal meeting (for dissemination and to establish
    624    co-operation). Review of deliverables due at month 18. Invited speaker
    625    from WCET community.
    626   \item \alert{Implementer's meeting, Edinburgh, December 2011}\\
    627    Discussion of issues found in the global proof strategy; introduction
    628    of the notion of structured traces and re-planning of the global
    629    proof strategy. Integration problems\\ addressed.
    630  \end{itemize}
    631 \end{frame}
    632589
    633590\end{document}
Note: See TracChangeset for help on using the changeset viewer.