Changeset 2007

May 30, 2012, 6:55:46 PM (5 years ago)

Potential workshop invitees

1 edited


  • Deliverables/D6.2/supplement.tex

    r2002 r2007  
    169169We have identified the following relevant groups to invite to the {\cerco}
    170 workshop.
     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.
     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.
     219\section{Publication Planning}
    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}
    188 \section{Publication Planning}
    190223A paper about...
    194227Dependent labelling
    196 The CerCo Frama-C plugin
    198 Automated analysis by CerCo of component reaction time in Lustre
     229The {\cerco} Frama-C plugin
     231Automated analysis by {\cerco} of component reaction time in Lustre
    200233Certifying compilation to object code (or is it certifying the costs?)
    204237Structured traces
    206 The CerCo formalisation
    208 A survey of CerCo results
     239The {\cerco} formalisation
     241A survey of {\cerco} results
     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.