source: Deliverables/Dissemination/final-review/wp6-notes.txt @ 3291

Last change on this file since 3291 was 3291, checked in by mckinna, 8 years ago

template beamer file, and notes for the talk
more later today!

File size: 2.8 KB
Line 
1In the final period of the \cerco\ project, a number of significant dissemination activities took place, in keeping with the culmination of the project, and the maturity of the ideas and methods developed.
2
3Two papers were presented at CPP, the leading emerging rival conference to ITP. The front-end semantics, presented as an executable function in \matita, by Brian Campbell (UEDIN), and the formalisation of the optimising assembler from the back-end by Mulligan and Sacerdoti Coen (UNIBO). UPD (Ayache, Amadio, R{\'gis} Giannis presented a paper on cost labelling of C programs at FMICS, the ERCIM working group workshop at FM 2012, the leading European conference on formal methods.
4
5In line with the reviewers' comments, and the Programme Manager's strong encouragement at the Paris review meeting in 2012, we orgainsed two meetings reported under Deliverables D6.4 and D6.5: Discussions between the site leaders at ETAPS in 2012 led to the proposal for a workshop at the 2013 ETAPS meeting in Rome, and while awaiting the outcome of the request for extension to accommodate that meeting, we identified HiPEAC in January 2013 in Berlin as a more industrially-oriented meeting at which to present \cerco\ results.
6
7Koen de Bosschere (UGent): e.g. security hardening an assembler to frustrate timing attacks.
8
9\matita\ now supports extraction, so we have fulfilled the reviewers' wish for a certified exectauble compiler, and this forms the trusted deliverable D5.2. Additionally, and itself no small endeavour, we have Debian packages and a live CD for the distribution and subsequent experimentation with, and exploitation of our technology.
10
11
12Dissemination:
13
14  \item direct: papers, presentations, workshops, software
15  \item indirect: ideas, people, follow-on projects
16
17Themes:
18
19  \item resource types, dependent types
20  \item source-level program analysis
21  \item formal verification
22  \item certifed code, certified analyses
23
24
25Origins/Destinations:
26
27We are part of an integrated research community; CerCo not a project in isolation:
28
29  \item FP5: IST 33149 ``Mobile Resource Guarantees''
30  \item FP6:
31        \item IST 015905 ``Mobius: Mobility, Ubiquity, Security''
32        \item FET-Open STReP 510255 ``EmBounded''
33  \item FP7: FET-Open STReP 243881 ``CerCo''
34  \item COST: ICT IC2102 ``TACLe''
35
36People/Projects
37
38  \item Pollack (Harvard): Crash/Safe (Pierce, Morrissett\ldots)
39  \item Campbell (UEDIN): REMS (Sewell, Cambridge)
40
41  \item
42
43Future of CerCo/CerCo in the future of ICT
44
45  \item \texttt{acc} as ``just another C compiler''
46  \item going with the grain of technology, not against it
47  \item from possibility-in-principle of formal verification to feasibility-in-practice
48
49  \item WCET in the future will be:
50        \item symbolic
51        \item local
52        \item modular
53        \item relativised: ``parametric'' in Lisper's words
Note: See TracBrowser for help on using the repository browser.