Changeset 2007


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

Potential workshop invitees

File:
1 edited

Legend:

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

    r2002 r2007  
    168168
    169169We have identified the following relevant groups to invite to the {\cerco}
    170 workshop.
     170workshop. 
     171\begin{itemize}
     172\item AbsInt.  AbsInt provide tools for validation of safety-critical
     173  software, including static analysis for worst-case execution time through
     174  abstract interpretation.  They have participated in a previous {\cerco}
     175  event, and their insights into the requirements for precise timing analysis
     176  are extremely relevant to the domain of {\cerco}.
     177\item Frama-C.  The \emph{Frama-C} platform for static analysis of C source
     178  code provides the context for the {\cerco} plugin which demonstrates the use
     179  of automated cost annotations on source code.
     180\item Rapita Systems. The \emph{RapiTime} timing analysis tool for real-time
     181  embedded systems uses runtime instrumentation of C to identify source-level
     182  execution costs and predict worst-cast execution time.
     183\item PASTA.  This research group at the University of Edinburgh are the
     184  designers of the \emph{EnCore} family of configurable embedded
     185  microprocessors.  Their \emph{ArcSim} tool offers cycle-accurate simulation
     186  of these low-energy cores, giving significant insights into the
     187  practicalities of precise cost analysis.
     188\item WCET-Aware Compilation.  Dr Heiko Falk at TU Dortmund leads this
     189  research project investigating the optimizations and compilation techniques
     190  appropriate to the requirements of worst-case rather than average-case
     191  timing.
     192\item Hume/EmBounded.  Prof. Kevin Hammond at the University of St Andrews
     193  leads a research team working on the quantification and certification of
     194  resource use in concurrent real-time embedded software.
     195\item ARM Verification Project.  Gordon, Fox and Myreen at the University of
     196  Cambridge have a machine-checked mathematical model of the ARM
     197  microprocessor.  With the release of the ARM Cortex-M series of low-power
     198  embedded processors, this is a potential application area for {\cerco}
     199  technology in the future.
     200\item CompCertTSO.  Sewell's group, also at the University of Cambridge, have
     201  a verified C compiler treating concurrency in a relaxed memory model.  Like
     202  {\cerco}, they have relevant experience of extending CompCert-based
     203  verification to additional code properties.
     204\item Artemis.  The European industry association \emph{Advanced Research \&
     205    Technology for Embedded Intelligence and Systems}.  We already have
     206  contact with Artemis through the University of Bologna, which is a member of
     207  the association.
     208\item IMDEA Software.  Dr Boris K\"opf applies quantitative analysis of code
     209  execution time to evaluate potential security weaknesses by side-channel
     210  attacks. 
     211\item ADSIG. The \emph{ArtistDesign Special Interest Group on Embedded Systems
     212    Design} is a large consortium of experts in embedded systems design,
     213  arising from the ARTIST Network of Excellence.
     214\end{itemize}
     215We propose to invite each of these groups to send participants and, if they
     216wish, contribute a short talk on their work to the afternoon session.
     217
     218
     219\section{Publication Planning}
    171220
    172221\hrule
    173222
    174 \begin{itemize}
    175 \item AbsInt
    176 \item Frama-C
    177 \item Rapita Systems
    178 \item Falk (WCET-aware compilation)
    179 \item PASTA EnCore / ARC / Arm
    180 \item St Andrews EmBounded Hume Hammond
    181 \item Fox / Myreen / Gordon - Cambridge ARM model - Sewell / x86-TSO CompCert TSO
    182 \item Artemis
    183 \item ADSIG - ArtistDesign Special Interest Group on Embedded Systems Design
    184 \item Köpf - IMDEA - quantitative analysis for timing attacks on security
    185 \end{itemize}
    186 
    187 
    188 \section{Publication Planning}
    189 
    190223A paper about...
    191224
     
    194227Dependent labelling
    195228
    196 The CerCo Frama-C plugin
    197 
    198 Automated analysis by CerCo of component reaction time in Lustre
     229The {\cerco} Frama-C plugin
     230
     231Automated analysis by {\cerco} of component reaction time in Lustre
    199232
    200233Certifying compilation to object code (or is it certifying the costs?)
     
    204237Structured traces
    205238
    206 The CerCo formalisation
    207 
    208 A survey of CerCo results
     239The {\cerco} formalisation
     240
     241A survey of {\cerco} results
    209242
    210243\end{document}
     244
     245%  LocalWords:  Frama AbsInt Rapita RapiTime EnCore ArcSim WCET Heiko
     246%  LocalWords:  Falk EmBounded Myreen CompCertTSO ADSIG ArtistDesign
Note: See TracChangeset for help on using the changeset viewer.