# Changeset 2007

Ignore:
Timestamp:
May 30, 2012, 6:55:46 PM (6 years ago)
Message:

Potential workshop invitees

File:
1 edited

Unmodified
Removed
• ## Deliverables/D6.2/supplement.tex

 r2002 We have identified the following relevant groups to invite to the {\cerco} workshop. workshop. \begin{itemize} \item AbsInt.  AbsInt provide tools for validation of safety-critical software, including static analysis for worst-case execution time through abstract interpretation.  They have participated in a previous {\cerco} event, and their insights into the requirements for precise timing analysis are extremely relevant to the domain of {\cerco}. \item Frama-C.  The \emph{Frama-C} platform for static analysis of C source code provides the context for the {\cerco} plugin which demonstrates the use of automated cost annotations on source code. \item Rapita Systems. The \emph{RapiTime} timing analysis tool for real-time embedded systems uses runtime instrumentation of C to identify source-level execution costs and predict worst-cast execution time. \item PASTA.  This research group at the University of Edinburgh are the designers of the \emph{EnCore} family of configurable embedded microprocessors.  Their \emph{ArcSim} tool offers cycle-accurate simulation of these low-energy cores, giving significant insights into the practicalities of precise cost analysis. \item WCET-Aware Compilation.  Dr Heiko Falk at TU Dortmund leads this research project investigating the optimizations and compilation techniques appropriate to the requirements of worst-case rather than average-case timing. \item Hume/EmBounded.  Prof. Kevin Hammond at the University of St Andrews leads a research team working on the quantification and certification of resource use in concurrent real-time embedded software. \item ARM Verification Project.  Gordon, Fox and Myreen at the University of Cambridge have a machine-checked mathematical model of the ARM microprocessor.  With the release of the ARM Cortex-M series of low-power embedded processors, this is a potential application area for {\cerco} technology in the future. \item CompCertTSO.  Sewell's group, also at the University of Cambridge, have a verified C compiler treating concurrency in a relaxed memory model.  Like {\cerco}, they have relevant experience of extending CompCert-based verification to additional code properties. \item Artemis.  The European industry association \emph{Advanced Research \& Technology for Embedded Intelligence and Systems}.  We already have contact with Artemis through the University of Bologna, which is a member of the association. \item IMDEA Software.  Dr Boris K\"opf applies quantitative analysis of code execution time to evaluate potential security weaknesses by side-channel attacks. \item ADSIG. The \emph{ArtistDesign Special Interest Group on Embedded Systems Design} is a large consortium of experts in embedded systems design, arising from the ARTIST Network of Excellence. \end{itemize} We propose to invite each of these groups to send participants and, if they wish, contribute a short talk on their work to the afternoon session. \section{Publication Planning} \hrule \begin{itemize} \item AbsInt \item Frama-C \item Rapita Systems \item Falk (WCET-aware compilation) \item PASTA EnCore / ARC / Arm \item St Andrews EmBounded Hume Hammond \item Fox / Myreen / Gordon - Cambridge ARM model - Sewell / x86-TSO CompCert TSO \item Artemis \item ADSIG - ArtistDesign Special Interest Group on Embedded Systems Design \item Köpf - IMDEA - quantitative analysis for timing attacks on security \end{itemize} \section{Publication Planning} A paper about... Dependent labelling The CerCo Frama-C plugin Automated analysis by CerCo of component reaction time in Lustre The {\cerco} Frama-C plugin Automated analysis by {\cerco} of component reaction time in Lustre Certifying compilation to object code (or is it certifying the costs?) Structured traces The CerCo formalisation A survey of CerCo results The {\cerco} formalisation A survey of {\cerco} results \end{document} %  LocalWords:  Frama AbsInt Rapita RapiTime EnCore ArcSim WCET Heiko %  LocalWords:  Falk EmBounded Myreen CompCertTSO ADSIG ArtistDesign
Note: See TracChangeset for help on using the changeset viewer.