Changes between Version 9 and Version 10 of HiPEAC13


Ignore:
Timestamp:
Jan 15, 2013, 11:21:18 AM (7 years ago)
Author:
campbell
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • HiPEAC13

    v9 v10  
    1919process to obtain a high level of assurance about the correctness and performance of the compiled code.
    2020
    21 The draft programme for the workshop consists of:
    22  * Short talks by !CerCo partners presenting the project and its results.
    23    * Project overview: a trustworthy framework for cost analysis of embedded
    24      code.
    25    * The labelling approach to cost analysis: a modular way to prove correctness;
    26      and methods to reason about the cost annotations and their application
    27 {{{
    28 #!comment
    29    * Demonstration of Frama-C plugin: high-level static reasoning about global
    30      runtime complexity.
    31    * Demonstration of Lustre plugin: automatic analysis of component reaction
    32      time.
    33 }}}
    34    * The verified !CerCo compiler: what makes a certified compiler trustworthy.
    35    * Dependent labels: managing refined cost information for richer
    36      architectures.
    37    * Future directions: the latest very-low-power embedded processors; other
    38      runtime costs; further languages.
    39  * Short presentations by some of the invited participants on the state of the
    40    art in static analysis of execution costs for embedded systems and future
    41    challenges.
     21
     22=== Programme ===
     23
     24|| 14:00-14:30 || Certified complexity: a general introduction (Claudio Sacerdoti Coen) ||
     25|| 14:30-15:15 || Certifying and reasoning on cost annotations of C programs (Yann Régis-Gianas) ||
     26|| 15:15-16:00 || Dealing with loop optimizations and pipelines (Paolo Tranquilli) ||
     27|| Break       || ||
     28|| 16:30-17:00 || Invited talk by Kevin Hammond ||
     29|| 17:00-17:30 || Certifying and reasoning on cost annotations of functional programs (Roberto Amadio) ||
     30|| 17:30-18:00 || A certified proof based on structured traces (Brian Campbell) ||
    4231
    4332=== Attendence ===