- Timestamp:
- May 17, 2013, 8:35:38 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/final-review/wp6-dissemination.ltx
r3300 r3301 28 28 \begin{frame}{Activities in the Third Period} 29 29 A number of distinct activities took place, as reported in D1.3/D1.4 30 and in the individual Deliverables already submitted. Noteworthy directoutcomes are:30 and in the individual Deliverables already submitted. Noteworthy \alert{direct} outcomes are: 31 31 32 32 \begin{description} … … 36 36 \end{description} 37 37 38 Indirectoutcomes:38 \alert{Indirect} outcomes: 39 39 \begin{description} 40 40 \item[people] a number of researchers moved on to other projects or industry 41 41 \item[ideas] executable semantics for CompCert C: Leroy, following Campbell (UEDIN) 42 42 \item[projects] COST Action TACLe (Lisper; SE), EPSRC REMS (Sewell, \textit{et al.}\ldots; UK) DARPA Crash/Safe (Morrissett \textit{et al.}\ldots; US) 43 \end{description} 44 45 \end{frame} 46 47 \begin{frame} 48 {Reflections} 49 \begin{description} 50 \item[HiPEAC] 51 \begin{description} 52 \item[+] well targeted: \textit{cf.} Koen de Bosschere (U.Gent) 53 \item[--] poorly attended 54 \end{description} 55 \item[ETAPS] 56 \begin{description} 57 \item[++] Intersection with PROARTIS (Vardanega) and TACLe (Lisper) 58 \item[-] scheduling/balance with QAPL meeting 59 \end{description} 60 \item[software] 61 \begin{description} 62 \item[++] Reusable, out-of-the-box installation; integration with Why3/Frama-C 63 \item[-] Quality of the extraction; refinements, improvements, completion of the proofs 64 \end{description} 65 \item[papers] 66 \begin{description} 67 \item[++] High quality! \textit{cf.} Leroy reusing Campbell's executable C semantics 68 \item[--] Challenge: identifying the target audience(s)? 69 \end{description} 70 \item[ideas] \begin{description} 71 \item[++] labelled source code; structured traces 72 \item[+/-] r{\^o}le of types in certification 73 \end{description} 43 74 \end{description} 44 75 … … 56 87 %%%\item COST: ICT IC2102 ``TACLe'' 57 88 \end{description} 58 former researchers on CerCo have moved to related research projects, or industrial formal methods groups:89 CerCo researchers now on related projects, or practising formal methods in industry: 59 90 \begin{description} 60 91 \item[UEDIN] 61 92 \begin{itemize} 62 \item Pollack, now researcher on Crash/Safe %%%(Morrissett \textit{et al.}\ldots; DARPA, US)63 \item Campbell, now researcher on REMS %%%(Sewell \textit{et al.}\ldots; EPSRC, UK)93 \item Pollack, now researcher on Crash/Safe (US)%%%(Morrissett \textit{et al.}\ldots; DARPA, US) 94 \item Campbell, now researcher on REMS (UK)%%%(Sewell \textit{et al.}\ldots; EPSRC, UK) 64 95 \end{itemize} 65 96 \item[UPD] \begin{itemize} 66 97 \item Ayache, engineer at CLEARSY (Atelier B, FR) 67 98 \item Bobot, researcher at CEA (Frama-C, FR) 99 \item Madet, researcher on PARKAS (INRIA, FR) 68 100 \end{itemize} 69 101 \item[UNIBO] \begin{itemize} 70 \item Tranquilli, to join Nokia (PL)102 \item Tranquilli, to join Nokia-Siemens Networks (PL) 71 103 \item Mulligan, now researcher on REMS (UK) 72 104 \item Boender, assistant professor at Middlesex (UK)
Note: See TracChangeset
for help on using the changeset viewer.