Changeset 3294 for Deliverables/Dissemination
- Timestamp:
- May 15, 2013, 4:18:17 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/final-review/wp6-dissemination.ltx
r3293 r3294 1 2 3 4 5 6 7 8 9 10 11 12 13 14 1 15 2 \begin{frame}{Summary} … … 18 5 19 6 \begin{description} 20 \item[direct] in the form of: 21 \begin{itemize} 22 \item Deliverables 7 \item[direct] in the form of Deliverables such as: 8 \begin{itemize} 23 9 \item papers 24 10 \item workshops 25 11 \item invited talks 26 12 \item software 27 \end{itemize} and 13 \end{itemize} 14 \\and\hfill\\ 28 15 \item[indirect] in the form of: 29 16 \begin{itemize} … … 51 38 \item[people] a number of researchers moved on to other projects or industry 52 39 \item[ideas] executable semantics for CompCert C: Leroy, following Campbell (UEDIN) 53 \item[projects] COST Action TACLe , EPSRC REMS, DARPA Crash/Safe40 \item[projects] COST Action TACLe (Lisper; SE), EPSRC REMS (Sewell, \textit{et al.}\ldots; UK) DARPA Crash/Safe (Morrissett \textit{et al.}\ldots; US) 54 41 \end{description} 55 42 … … 57 44 58 45 \begin{frame}{Research Context: Projects and People} 59 CerCo is not an isolated project, but builds on existing established networks of nationally- and EU-funded research: for example, 60 \begin{itemize} 46 Building on established networks of EU-funded research: \begin{itemize} 61 47 \item FP5: IST 33149 ``Mobile Resource Guarantees'' 62 \item FP6: 48 \item FP6: \begin{itemize} 63 49 \item IST 015905 ``Mobius: Mobility, Ubiquity, Security'' 64 50 \item FET-Open STReP 510255 ``EmBounded'' 51 \end{itemize} 65 52 \item FP7: \red{FET-Open STReP 243881 ``CerCo''} 66 \item COST: ICT IC2102 ``TACLe''53 %%%\item COST: ICT IC2102 ``TACLe'' 67 54 \end{itemize} 68 69 Similarly, a number of research projects, or idnustrially-related formal methods grousp, now employ researchers formerly attached to CerCo: 55 former researchers on CerCo have moved to related research projects, or industrial formal methods groups: 70 56 \begin{description} 71 57 \item[UEDIN] 72 58 \begin{itemize} 73 \item Pollack, now on Crash/Safe(Morrissett \textit{et al.}\ldots; DARPA, US)74 \item Campbell, now on REMS(Sewell \textit{et al.}\ldots; EPSRC, UK)59 \item Pollack, now researcher on Crash/Safe %%%(Morrissett \textit{et al.}\ldots; DARPA, US) 60 \item Campbell, now researcher on REMS %%%(Sewell \textit{et al.}\ldots; EPSRC, UK) 75 61 \end{itemize} 76 62 \item[UPD] \begin{itemize} 77 \item Ayache, formal mthodsengineer at CLEARSY (Atelier B, FR)63 \item Ayache, engineer at CLEARSY (Atelier B, FR) 78 64 \item Bobot, researcher at CEA (Frama-C, FR) 79 65 \end{itemize} 80 66 \item[UNIBO] \begin{itemize} 81 \item Tranquili, 67 \item Tranquilli, to join Nokia (PL) 68 \item Mulligan, now researcher on REMS (UK) 69 \item Boender, assistant professor at Middlesex (UK) 82 70 \end{itemize} 83 71 \end{description} … … 85 73 \end{frame} 86 74 87 88 89 \begin{frame}{} 90 91 \end{frame} 92 75 \begin{frame}{Prospects for further exploitation} 76 In addition to the movement of people, and influence of ideas already sketched: 77 \begin{description} 78 \item[further proof/software development] UNIBO, with existing staff 79 \item[more advanced hardware models] UNIBO, as above, UEDIN with REMS 80 \item[further collaborations] COST: ICT IC2102 ``TACLe'' (Lisper, SE). UNIBO and UEDIN 81 \end{description} 82 In particular, the role of source-level (timing) analysis in the future of WCET, envisaged as ``parametric'': 83 \begin{itemize} 84 \item symbolic 85 \item local, modular 86 \item relativised (\textit{cf.} dependent labelling) 87 88 \end{itemize} 89 \end{frame} 93 90 94 91
Note: See TracChangeset
for help on using the changeset viewer.