Changeset 3294 for Deliverables/Dissemination

Timestamp:

May 15, 2013, 4:18:17 PM (7 years ago)

Author:

mckinna

Message:

draft final version: more to say than to put on slides etc.

File:

• Deliverables/Dissemination/final-review/wp6-dissemination.ltx (modified) (5 diffs)

Deliverables/Dissemination/final-review/wp6-dissemination.ltx

@@ -1 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
 
 \begin{frame}{Summary}
@@ -18 +5 @@
 
 \begin{description}
-\item[direct] in the form of: 
-  \begin{itemize}
-  \item Deliverables
+\item[direct] in the form of Deliverables such as: 
+  \begin{itemize}
   \item papers
   \item workshops
   \item invited talks
   \item software
-  \end{itemize} and
+  \end{itemize}
+\\and\hfill\\
 \item[indirect] in the form of:
   \begin{itemize}
@@ -51 +38 @@
   \item[people] a number of researchers moved on to other projects or industry
   \item[ideas] executable semantics for CompCert C: Leroy, following Campbell (UEDIN)
-  \item[projects] COST Action TACLe, EPSRC REMS, DARPA Crash/Safe
+  \item[projects] COST Action TACLe (Lisper; SE), EPSRC REMS (Sewell, \textit{et al.}\ldots; UK) DARPA Crash/Safe (Morrissett \textit{et al.}\ldots; US)
   \end{description}
 
@@ -57 +44 @@
 
 \begin{frame}{Research Context: Projects and People}
-CerCo is not an isolated project, but builds on existing established networks of nationally- and EU-funded research: for example, 
-\begin{itemize}
+Building on established networks of EU-funded research: \begin{itemize}
   \item FP5: IST 33149 ``Mobile Resource Guarantees''
-  \item FP6: 
+  \item FP6: \begin{itemize}
         \item IST 015905 ``Mobius: Mobility, Ubiquity, Security''
         \item FET-Open STReP 510255 ``EmBounded''
+        \end{itemize}
   \item FP7: \red{FET-Open STReP 243881 ``CerCo''}
-  \item COST: ICT IC2102 ``TACLe''
+  %%%\item COST: ICT IC2102 ``TACLe''
 \end{itemize}
-
-Similarly, a number of research projects, or idnustrially-related formal methods grousp, now employ researchers formerly attached to CerCo: 
+former researchers on CerCo have moved to related research projects, or industrial formal methods groups: 
 \begin{description}
 \item[UEDIN]
   \begin{itemize}
-  \item Pollack, now on Crash/Safe (Morrissett \textit{et al.}\ldots; DARPA, US)
-  \item Campbell, now on REMS (Sewell \textit{et al.}\ldots; EPSRC, UK)
+  \item Pollack, now researcher on Crash/Safe %%%(Morrissett \textit{et al.}\ldots; DARPA, US)
+  \item Campbell, now researcher on REMS %%%(Sewell \textit{et al.}\ldots; EPSRC, UK)
   \end{itemize}
 \item[UPD] \begin{itemize}
-  \item Ayache, formal mthods engineer at CLEARSY (Atelier B, FR)
+  \item Ayache, engineer at CLEARSY (Atelier B, FR)
   \item Bobot, researcher at CEA (Frama-C, FR)
   \end{itemize}
 \item[UNIBO] \begin{itemize}
-  \item Tranquili, 
+  \item Tranquilli, to join Nokia (PL)
+  \item Mulligan, now researcher on REMS (UK)
+  \item Boender, assistant professor at Middlesex (UK)
   \end{itemize}
 \end{description}
@@ -85 +73 @@
 \end{frame}
 
-
-
-\begin{frame}{}
-
-\end{frame}
-
+\begin{frame}{Prospects for further exploitation}
+  In addition to the movement of people, and influence of ideas already sketched:
+  \begin{description}
+  \item[further proof/software development] UNIBO, with existing staff
+  \item[more advanced hardware models] UNIBO, as above, UEDIN with REMS
+  \item[further collaborations] COST: ICT IC2102 ``TACLe'' (Lisper, SE). UNIBO and UEDIN
+  \end{description}
+  In particular, the role of source-level (timing) analysis in the future of WCET, envisaged as ``parametric'': 
+  \begin{itemize}
+    \item symbolic
+    \item local, modular
+    \item relativised (\textit{cf.} dependent labelling) 
+
+  \end{itemize}
+\end{frame}