Changes between Initial Version and Version 1 of HiPEAC13


Ignore:
Timestamp:
Nov 21, 2012, 12:12:22 PM (7 years ago)
Author:
campbell
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • HiPEAC13

    v1 v1  
     1= !CerCo: Certifying Costs in a Certified Compiler =
     2== HiPEAC 2013 half-day workshop ==
     3
     4The !CerCo workshop considers the construction of formally verified compilers
     5for embedded systems that can be used to certify timing bounds at the level
     6of ''source'' code. 
     7
     8The workshop has two objectives:
     9 * To publicise the results of [WikiStart CerCo FP7 project] to members of the relevant
     10   industrial and academic research communities.
     11 * To stimulate discussion between the industrial and academic participants
     12   about future work building on the current state of the art.
     13
     14The !CerCo project links a low level cycle precise execution time analysis with an innovative
     15source code labelling approach that presents the results of the timing analysis in
     16annotated source code.  This allows high level reasoning about the execution time of
     17compiled programs.  We combine this with formal verification of the compilation
     18process to obtain a high level of assurance about the correctness and performance of the compiled code.
     19
     20The draft programme for the workshop consists of:
     21 * Short talks by !CerCo partners presenting the project and its results.
     22   * Project overview: a trustworthy framework for cost analysis of embedded
     23     code.
     24   * The labelling approach to cost analysis: a modular way to prove correctness;
     25     and methods to reason about the cost annotations and their application
     26{{{
     27#!comment
     28   * Demonstration of Frama-C plugin: high-level static reasoning about global
     29     runtime complexity.
     30   * Demonstration of Lustre plugin: automatic analysis of component reaction
     31     time.
     32}}}
     33   * The verified !CerCo compiler: what makes a certified compiler trustworthy.
     34   * Dependent labels: managing refined cost information for richer
     35     architectures.
     36   * Future directions: the latest very-low-power embedded processors; other
     37     runtime costs; further languages.
     38 * Short presentations by some of the invited participants on the state of the
     39   art in static analysis of execution costs for embedded systems.
     40 * Conclusion: Round-table discussion on potential applications and future
     41   challenges.
     42
     43=== Attendence ===
     44
     45Participation in the workshop is open.  It is taking place as part of the
     46[http://www.hipeac.net/conference/berlin HiPEAC 2013 conference in Berlin],
     47January 21‐23, 2013.  All attendees should register for the main conference.
     48
     49=== Organizers and their affiliations ===
     50
     51 * [http://www.cs.unibo.it/~sacerdot Claudio Sacerdoti Coen], University of Bologna, Italy
     52 * [http://homepages.inf.ed.ac.uk/stark/ Ian Stark], University of Edinburgh, UK
     53 * [http://www.pps.jussieu.fr/~amadio/ Roberto Amadio], Université de Paris Denis Diderot, France