Changeset 1850


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

...

File:
1 edited

Legend:

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

    r1848 r1850  
    6969   \alert{\Large
    7070   \begin{itemize}
    71     \item Maximal expressivity (precison) in the specification
     71    \item Maximal expressivity (precision) in specification
    7272    \item Interactive proofs
    7373    \item Abstraction, loss of precision as special cases of specification
     
    132132
    133133\begin{frame}
    134  \frametitle{Short term objectives}
     134 \frametitle{Short term objectives (achievements)}
    135135 \begin{enumerate}
    136136  \item develop a \alert{compiler} from
    137         \alert{$\approx\!\!$ C} to the \alert{MCS-51} microprocessor
    138         used for embedded systems (achieved in 1st period)
     137        \alert{$\approx\!\!$ C} to \alert{MCS-51} processor
     138        (1st period)
    139139  \item have the compiler infer from the assembly code a \alert{precise cost
    140         model} for the source program (achieved in 1st period)
     140        model} for the source program (1st period)
    141141  \item \alert{certify} the compiler
    142142  \item embed the compiler in a \alert{prototypical environment} for
     
    144144    \item stating \alert{cost invariants} based on the inferred cost model
    145145    \item computing \alert{proof obligations}
    146     \item \alert{proving} automatically or interactively the generated proof obligations
     146    \item \alert{proving} generated obligations automatically or interactively
    147147   \end{itemize}
    148    (partially achieved in 2nd period)
    149   \item lift the technique to a \alert{synchronous languages} (e.g. Esterel)
    150         compiled via C (achieved in 2nd period)
     148   (partially in 2nd period)
     149  \item lift the technique to a \alert{synchronous language}
     150        (2nd period)
    151151  \item \alert{Scale} the approach to \alert{more complex scenarios}
    152152 \end{enumerate}
     
    175175 Main practical achievements (D2.2):
    176176 \begin{center}
    177   \alert{\Large an untrusted compiler from C-Light to the MCS-51 microprocessor
     177  \alert{\Large an untrusted compiler from C-Light to the MCS-51 processor
    178178   that implements the methodology}
    179179 \end{center}
     
    185185 \begin{center}
    186186  \alert{\Large formalized executable semantics for C-Light and the MCS-51
    187    microprocessor}
     187   processor}
    188188 \end{center}
    189189\end{frame}
     
    257257 \begin{enumerate}
    258258  \item Loop optimization\\
    259    \alert{the program state is always known and availale on the source code}\\
     259   \alert{program state always known and available in the source code}\\
    260260   Total precision can be achieved.\\
    261261   Problem: are the dependent annotations easy to understand and work with
    262262   (manually or automatically)? Probably yes
    263263 \item Cache\\
    264    \alert{the cache state can only (?) be approximated (via abstract interpretation)}\\
     264   \alert{\makebox[0pt][l]{cache state only (?) approximated (via abstract interpretation)}}\\
    265265   Total precision impossible (?) to achieve\\
    266266   Problem: are the dependent annotations easy to understand and work
     
    271271\begin{frame}
    272272 \frametitle{Recommendations from the reviewers: action taken}
    273  We hired Dr. Paolo Tranquilli (UNIBO) at month 19 to
     273 Dr. Paolo Tranquilli hired at UNIBO at month 19 to
    274274 \begin{itemize}
    275275  \item Develop the dependent labelling approach (completed)
     
    291291 \frametitle{Recommendations from the reviewers: action taken}
    292292 \alert{No impact on planning}\\
    293  Dr. Tranquilli and Dr. Boender (Post-Docs) were hired by UNIBO in place of the
    294  senior researcher whose hiring was made impossible during the first period.\\
     293 Dr. Tranquilli and Dr. Boender (Post-Docs) replaced the
     294 senior researcher position which was made impossible during the first period.\\
    295295 ~\\
    296296
     
    406406
    407407\begin{frame}
    408  \frametitle{Achievements (2nd period) 1/3, Ayache's talk}
     408 \frametitle{Achievements (2nd period) 1/3, Ayache}
    409409 From the \alert{CerCo annotating compiler} (1st period)\\
    410410 ~~~~~ - inference of costs for basic blocks;\\
     
    428428
    429429\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\\
     430 \frametitle{Achievements (2nd period) 2/3, Mulligan/Campbell}
     431 Towards the \alert{CerCo trusted prototype} (3rd period): to verify\\
     432 ~~~ - preservation of labelled traces;\\
     433 ~~~ - exact correspondence between actual and inferred cost\\
    435434 \begin{enumerate}
    436435  \item CIC encoding: Front/Back end (D4.2/D4.3)
     
    442441    \item \alert{Optimizing assembler} verification (75\%)
    443442    \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)
     443    \item Generation of \alert{structured} labelled traces (for
     444          back-end)\\ from \alert{flat} labelled traces (from front-end)
    446445   \end{itemize}
    447446 \end{enumerate}
     
    449448
    450449\begin{frame}
    451  \frametitle{Achievements (2nd period) 3/3 R\`egis-Gianas/Tranquilli talks }
     450 \frametitle{Achievements (2nd period) 3/3 R\`egis-Gianas/Tranquilli}
    452451 \alert{Enlarging the scope} of CerCo techniques
    453452 \begin{enumerate}
     
    505504 \begin{enumerate}
    506505  \item Research on dependent labelling in response to reviewers.\\
    507     \alert{No impact on the schedule, work performed by additional Post-Doc.}
     506    \alert{No impact on the schedule, work done by additional Post-Doc.}
    508507  \item Bring forward D5.3 from the third to the second period.\\
    509508    D5.3 is a major case study to assess the potential
     
    526525 Management WP1:
    527526 \begin{enumerate}
    528   \item to \alert{coordinate and supervise} activities to be
     527  \item \alert{coordinate and supervise} activities to be
    529528    carried out
    530   \item to carry out the overall \alert{administrative and
     529  \item carry out the overall \alert{administrative and
    531530    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
     531  \item manage \alert{contacts with the European Commission}
     532  \item \alert{monitor quality and timing} of project deliverables
     533  \item establish effective internal and external
    535534        \alert{communication procedures}
    536535 \end{enumerate}
Note: See TracChangeset for help on using the changeset viewer.